Count positive correlation for overlapping ternary full guards (no κ)

research/ranktwo-overlap-ternary/README.md

@@ -0,0 +1,175 @@
+# Positive correlation for overlapping ternary rank-two full guards
+
+This package was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: exact finite certificate with a written counting reduction.**
+For the fixed commuting projectors over F3
+
+```text
+P = diag(0,1,0,1),   Q = diag(0,0,1,1),
+```
+exactly **2,409,984 of 24,261,120** complete headers in GL4(F3) pass
+both requests' full guards. Their joint fraction is **523/5265**.
+Each marginal is **361/1170**, so their covariance is strictly positive:
+
+```text
+523/5265 - (361/1170)^2 = 5659/1368900 > 0.
+```
+
+A request passes G when the leading principal minors of GPG^-1 or GQG^-1
+of orders one and two are both nonzero. This is a fixed, uniform complete
+header cover and a fixed pair chosen before the header. The result applies
+to every commuting ternary projector pair with joint-sector dimensions
+(00,10,01,11) = (1,1,1,1), by simultaneous conjugation.
+
+This supplies an explicit positive-correlation example beyond the orthogonal
+and corank-one families. It answers one bounded part of the nonlaminar
+full-guard question and gives a new residual-state fixture for state-aware
+recursion. No new kappa, supplier admission or multiplication theorem follows.
+
+## Exact residual distribution
+
+After a passing first pivot, each Schur complement is a rank-one idempotent
+on F3^3. In the following table S and T are ordered. The middle count is the
+number of first split pairs reaching that type. The next column counts
+second split pairs passing both terminal guards, out of 234. Multiplication
+by 48 gives the passing complete GL3 continuation headers per first split.
+
+| Residual type | First splits | Passing second splits | Full GL4 headers |
+|---|---:|---:|---:|
+| S = T | 44 | 114 | 240,768 |
+| Same image, different kernels | 88 | 78 | 329,472 |
+| Same kernel, different images | 88 | 78 | 329,472 |
+| ST = TS = 0 | 294 | 44 | 620,928 |
+| ST = 0, TS != 0 | 168 | 50 | 403,200 |
+| TS = 0, ST != 0 | 168 | 50 | 403,200 |
+| Different images/kernels, tr(ST) = 1 | 32 | 54 | 82,944 |
+| Different images/kernels, tr(ST) not in {0,1} | 0 | 56 | 0 |
+| Total | 882 | | 2,409,984 |
+
+The table's terminal counts are the specialization of Nick Petalas's
+[#4240 rank-one pair law](../projector-pair-header-law/README.md).
+The new quantities are the initial residual distribution, its weighted
+full-guard count and the positive covariance. The verifier computes the
+second-split count separately for **every** initial split; its total does
+not assume that a residual type is a sufficient invariant or use the
+predecessor formula to generate successful events. In particular, generic
+residuals occur zero times in this enumerated domain only.
+
+## Counting reduction
+
+1. Write x=e1^T G and y=G^-1 e1. Then xy=1. There are
+   (3^4-1)3^3=2160 such pairs. For each, choose W=[y,B], where B is the
+   explicit ordered basis of ker x in the verifier. Thus xW=e1^T and
+   G0=W^-1 has first row x. Every header with this same split pair has
+   the unique form diag(1,K)G0 for K in GL3(F3). This proves the common
+   completion factor |GL3(F3)|=11232 and total denominator 24,261,120.
+
+2. For either conjugated request R=G0 P G0^-1 or G0 Q G0^-1, write
+   R=[[p,b],[c,D]]. When p is nonzero its Schur complement is
+   S=D-cb/p. The leading two-by-two determinant after the remaining
+   change K is p times (K S K^-1)[0,0]. Therefore the two full guards
+   are equivalent to both initial pivots being nonzero and both
+   residual first pivots being nonzero. Standard idempotent Schur
+   deletion gives rank one; the verifier also checks nonzero rank and
+   S^2=S at every applicable split. This scalar deletion is credited
+   to the retained #4228/#4278 lineage.
+
+3. Put a=e1^T K and b=K^-1 e1 in dimension three. There are
+   (3^3-1)3^2=234 split pairs ab=1, each with exactly |GL2(F3)|=48
+   completions by the same basis argument. Count the terminal events
+   by directly evaluating aSb and aTb. The verifier visits all
+   2160*234=505440 two-stage split paths. The successful totals before
+   the final completion multiplier are 155952 for either marginal
+   and 50208 for their intersection. Consequently the full counts
+   are 7,485,696 for either marginal and 2,409,984 jointly.
+
+4. All idempotent commuting pairs with the stated four sector dimensions
+   are simultaneously conjugate to P,Q. Multiplication of G by a fixed
+   conjugating matrix permutes the complete GL4 cover. Thus the count
+   depends on that sector profile, rather than the chosen axis labels.
+
+This proof reduces an exact finite enumeration to its explicitly enumerated
+finite domain; it does not assert a formula uniform in field size or rank.
+
+## Reproduction and evidence
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/ranktwo-overlap-ternary/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/ranktwo-overlap-ternary/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ranktwo-overlap-ternary
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ranktwo-overlap-ternary --check-source-history
+```
+
+The verifier prints `PASS_RANKTWO_OVERLAP_TERNARY` in a generated JSON receipt
+binding every package file's SHA256. It writes no files. The registered
+normal and optimized runs use explicit exceptions, so -O retains every check.
+
+Besides the complete two-stage split enumeration, the verifier scans all
+19,683 ternary three-by-three matrices to obtain GL3. For one original split
+in each of the seven occupied residual types, it checks all 11,232 literal
+complete headers in the continuation fibre. These **78,624** direct header
+checks evaluate the original requests' one-by-one and two-by-two minors
+without Schur complements. They corroborate each class's continuation count;
+this is not a raw scan of all 24,261,120 GL4 headers.
+
+Reversing the completion kernel basis preserves the residual type for every
+one of the 882 jointly admitted first splits. Eight controls cover a singular
+matrix, two invalid split pairs, a zero pivot, loss of continuation information
+under commutator-only state identification, first-pivot/full-guard confusion,
+a missing completion multiplier and the complete denominator.
+
+Power of Ten scope is this standalone verifier. Its dimension is fixed at
+four, its field at three, functions are below 60 lines, and it uses no recursion,
+subprocesses or runtime-generated code. Every loop is bounded by these fixed
+domains; the largest raw scan is 19,683 matrices. Python's managed allocation
+requires a rule 3 deviation: the live GL3 list is bounded at 11,232 matrix/inverse
+pairs, first splits at 2160 and terminal splits at 234; there is no user-selected
+size. A fixed-capacity implementation is a follow-up only if these bounds change.
+Warning-strict execution and the repository's package checks provide available
+Python diagnostics; no new repository-wide analyzer configuration is introduced.
+
+## Scope, predecessor credit and limitations
+
+This takes the nonlaminar question of Nick Petalas #4240/#4259 and the
+state-aware continuation question of **ssafwann #4678**, **Mihir Srivastava
+#4689**, and **codyw912 #4735**. Their one-block, binary rank-three profile and
+binary transition results retain their credit. **MatShep #4762** supplies the
+related all-field factor-invariant framework. None of those results is the
+deliverable being rechecked here, and none of their executable code is imported.
+
+Credit Nick Petalas's #4240 terminal law and #4228/#4278 scalar completion/Schur
+lineage; **Ryanson Jonathan** for the separate-family full-guard census and
+sharpness work; **lee-phys** for dimension work; **Cinna Davis** for the BIT
+request context; and **source527**, **commdata2338**, and **Jose Manuel** for
+the normalizer lineage. Exact main-source blobs are historical provenance in
+[SOURCES.json](SOURCES.json). Their original credit lines remain unchanged.
+
+Canonical base is 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7.
+[TASK.json](TASK.json) marks formal-interface-lemma as changed to this algebraic
+side result. The card's old balanced-transfer baseline fails on the current
+certificate with KeyError 'bit_lower'; its documented replacement
+`research_selected_baseline.py` passes source-binding orientation. Neither
+baseline is scientific evidence for this count.
+
+Finite exactness is the claim. Other fields, sector profiles, restricted or
+weighted header covers and adaptive requests remain outside scope. Ternary
+rank two is within the odd-field algebraic model, but no actual producer,
+header selection/emission, physical reads, dirty restoration, stock, dispatch
+or complete consumer bill is provided. No selected scientific cold replay,
+Lean or Docker run is required or claimed. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. Determine an exact field-uniform law for this same four-sector pair.
+   This would identify when its positive correlation persists. Start by
+   counting the residual-type multiplicities symbolically from sector dot
+   products; the missing ingredient is that distribution, rather than the
+   already known terminal rank-one laws.
+2. Extend a state-aware recursion to one larger nonlaminar profile using
+   #4762's factor invariant. First retain actual transition multiplicities
+   and compare them with a literal finite sample. A complete higher-rank
+   transition law and its cost remain missing.

research/ranktwo-overlap-ternary/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/projector-pair-header-law/README.md",
+      "usage": "provenance",
+      "git_blob": "e8b79e95d0ee8105d3c931766eaf53e45a680005",
+      "sha256": "49e2f01d95f856e366fd254320b78fa7e48dbad622b605fe2222b5755c403156"
+    },
+    {
+      "path": "research/laminar-header-law/README.md",
+      "usage": "provenance",
+      "git_blob": "b39ea17c2764764e507d8d3c8b2f079dc2a96efa",
+      "sha256": "5cf3ff2b00615c59c8a534552517eeab966bcdd8e7b5029aaa1919b4fb942d09"
+    },
+    {
+      "path": "research/schur-header-count/README.md",
+      "usage": "provenance",
+      "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2",
+      "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e"
+    },
+    {
+      "path": "research/schur-residual-orbits/README.md",
+      "usage": "provenance",
+      "git_blob": "a2361477d9373969ccb7ab0f4f3c4b9919c051ba",
+      "sha256": "15e2f1a7d4edcc8f71e75ead949928c2ac883a3fb8268bb5827f290de4d28d76"
+    },
+    {
+      "path": "research/schur-invariant-transitions/README.md",
+      "usage": "provenance",
+      "git_blob": "d5118b9f5911949964245eb8942065faff972900",
+      "sha256": "fccdd2bff1ee00c120796bb1b6c3739cce90dcffbff7c96e897300ed81bba72e"
+    },
+    {
+      "path": "research/idempotent-factor-invariant/README.md",
+      "usage": "provenance",
+      "git_blob": "48ce67bdc3c7c35081cc04f86b7ee20c6a5dd06b",
+      "sha256": "fae88ccbea3a16d041666f5956d0416b6a21ef57a21f1a0996c7c3a74f7fa3d1"
+    }
+  ]
+}

research/ranktwo-overlap-ternary/TASK.json

@@ -0,0 +1,128 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact finite full-guard count and positive covariance for the ternary commuting rank-two projector pair with joint sectors (1,1,1,1).",
+  "scope_change_reason": "Take the explicit nonlaminar full-guard and state-continuation questions as an algebraic side result; no proof-assistant or selected caller claim.",
+  "bottleneck_link": "The joint law supplies a new nonlaminar state-aware header fixture; it alone supplies no paid header cover or supplier improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original finite result; leave field-uniform and larger-profile laws as open questions.",
+  "outcome": "completed",
+  "evidence": "505440 enumerated two-stage split paths and 78624 literal complete-header checks, with exact residual multiplicities and positive covariance.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the field-uniform full-guard law for this four-sector pair?",
+      "why_it_matters": "It would classify persistence of positive correlation.",
+      "first_step": "Count initial residual types symbolically using sector dot products.",
+      "blocked_by": "An exact field-uniform residual distribution."
+    },
+    {
+      "question": "Can the factor invariant yield an explicit next-pivot law for a larger nonlaminar profile?",
+      "why_it_matters": "This is needed for scalable state-aware header recursion.",
+      "first_step": "Choose one profile, retain multiplicities and compare literal samples.",
+      "blocked_by": "Higher-rank transition multiplicities and complete physical costs."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132056",
+  "upstream_refresh": {
+    "commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+    "priority_revision": 7,
+    "utc": "2026-10-22T20:13:41Z"
+  },
+  "overlap": {
+    "open_prs": 326,
+    "discussion_records": 3754,
+    "coverage_time": "2026-10-22T20:19:43.415699+00:00",
+    "local_notes": 119,
+    "head_notes": 6319,
+    "limits": "Sparse local-note coverage; main README searches supplement it. Arbitrary diffs and unpublished work excluded. Merged PR searches checked rank-two header, Schur count and residual orbit terms."
+  },
+  "preserved_prior_branch": "research/w6-1022g-header-extension",
+  "preserved_prior_head": "9997ae7d1c99ecf5eb915aad28eb7b61e778956c",
+  "claim_type": "exact finite certificate with written reduction",
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS 27.0.1 arm64",
+    "requirements": "standard library only"
+  },
+  "local_check_times_seconds": {
+    "normal": 1.27,
+    "optimized": 1.27,
+    "registered_total": 2.86
+  }
+}

research/ranktwo-overlap-ternary/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact split enumeration, literal complete-header fibres, residual types, positive covariance and eight semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical finite certificate with assertions disabled; every contract remains active."
+    }
+  ]
+}