Prove two centre-kernel cosets cannot improve compression density (no new κ)

research/centre-two-coset-separation/PROOF.md

@@ -0,0 +1,148 @@
+# Two left cosets cannot create an additional centre-kernel direction
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof, with a source-bound finite premise and
+small exact corroboration. Independent human and formal proof-kernel review
+are unclaimed. The theorem is about the historical scalar observation
+contract of PR3071/3291/3656/3797/3828, not the current P104 native word.
+
+## 1. Contract and inherited premises
+
+Let G act regularly on its owner labels, let H be a finite subgroup, and let
+rho_p be involutions indexed by ports p. Work over Q or C. R_p is a column
+of a fixed reader R. For inputs supported on B, retain every later output,
+including outputs outside B, and put
+
+```text
+Sx(g)  = sum_p R_p x(g,p),
+4Tx(z) = sum_p R_p x(z rho_p,p).
+```
+
+For D={a,b,c}, suppose the following conditions hold.
+
+1. The right-coset partition of the ports by H rho_p consists of D and
+   singleton classes. H is generated by rho_a rho_b and rho_a rho_c.
+2. R_D has rank two with kernel generated by u=(1,-1,-1).
+3. Every pair of distinct reader columns is linearly independent.
+4. For W=span(R_a,R_b), every R_p with p outside D is outside W.
+
+The single-block coset classification, subgroup order 4080, reader rank
+eight, and one constant triple direction per left translate are **cited
+premises**, from Clear1nsight's PR3828 and Ross Richardson's PR3797.
+Sagar Thakrar's PR3291, through PR3071's source reader, supplies the
+nonparallel-column premise. These predecessor results are not audited here.
+Matarener's PR3656 supplies the original subgroup and constant witness.
+
+Condition 4 is the additional source check. On the authenticated reader,
+exact elimination gives rank(R_0,R_6,R_p)=3 for each of the 109 ports outside
+{0,6,85}, and rank two for those three ports. The program extracts R from
+the archived canonical prefix using the retained query convention. It does
+not execute a predecessor verifier or repeat the group/coset census.
+
+## 2. Separation lemma
+
+Let B_1=sH and B_2=tH be distinct left cosets. They are disjoint. At any
+fixed later output z, the ports arriving from B_i are either absent, one
+singleton port, or exactly D. This follows from the right-coset partition
+after left translation by s or t.
+
+There are two additional exclusions.
+
+* If both blocks contribute singleton ports p and q, then p differs from q.
+  Indeed, B_1 rho_p and B_2 rho_p are disjoint, since right multiplication
+  by rho_p is a bijection.
+* Both blocks cannot contribute D at the same z. Their triple output sets
+  are B_1 rho_a and B_2 rho_a, which are disjoint by the same bijection.
+
+Now impose Tx(z)=0. If only a singleton arrives, its coefficient is zero.
+For two singletons, pairwise independence of R_p,R_q makes both
+coefficients zero. For one singleton and one triple, the triple's response
+lies in W and the singleton's column lies outside W, so its coefficient
+is zero. These exhaust every output equation that contains a singleton.
+Every source coordinate on a singleton port appears at its own output
+z=g rho_p. Consequently all source coordinates outside D vanish.
+
+This argument allows arbitrary partial intersections of the translated
+outgoing sets. It assumes neither normality of H nor that those sets form
+one common quotient partition after translation.
+
+## 3. Exact kernel on two blocks and their subblocks
+
+Once all singleton coordinates vanish, the source equation gives
+
+```text
+x(g,p) = alpha(g) u_p, p in D.
+```
+
+There is no cross-block triple output. Therefore the later equations
+reduce separately on B_1 and B_2 to
+
+```text
+alpha(g) = alpha(g rho_a rho_b) = alpha(g rho_a rho_c).
+```
+
+Both products generate H. The right Cayley graph on each left coset is
+connected, so alpha is constant separately on each block. Conversely each
+constant triple vector has zero S and T, as in the cited one-block witness.
+Their source supports are disjoint, so the vectors are independent. Thus
+
+```text
+ker(S on B_1 union B_2) intersect ker(T on B_1 union B_2)
+  = span{1_(B_1) tensor u, 1_(B_2) tensor u},
+dimension = 2.
+```
+
+This holds for **every** pair of distinct left cosets. It is not a finite
+enumeration of relative translations.
+
+For any A contained in B_1 union B_2, extend its inputs by zero. The theorem
+then says that its kernel has dimension j, where j is the number of these
+two cosets contained in A in full. Omitting any owner of one block forces
+that block's constant amplitude to vanish. This is an immediate support
+corollary, without an additional search or a hypothesis about missing outputs.
+
+For the cited 112-port, rank-eight reader, dim ker(S_A)=104|A|. Hence
+
+```text
+rank(T_A restricted to ker(S_A)) = 104|A| - j.
+```
+
+This is the exact minimum number of additional **scalar linear**
+observations that, together with S, determine the whole T field. A lower
+count leaves an ambiguity in ker S outside ker T, even if postprocessing
+is nonlinear. A linear quotient by the common kernel attains the count
+abstractly. There is no assertion of efficient physical access or decoding.
+
+For two full source cosets, |A|=8160 and j=2, so the minimum is
+848638. These are derived counts from the theorem and cited source order,
+not a claim to have eliminated the full 913920-variable matrix.
+The invisible fraction remains exactly 1/424320 of ker S. Pairing two
+blocks cannot improve the single-block information-compression density.
+
+## 4. Executable corroboration and limits
+
+The source check establishes only condition 4 and the distinguished relation.
+The other actual-source premises are inherited as stated in section 1.
+
+The new implication is corroborated over Q on G=S3 times C2, with
+H=A3 times {0}. The three D routes are the three transpositions with zero
+C2 bit. Two singleton routes are (identity,1) and (first transposition,1).
+Their columns are e3 and e4, while the D columns are e1+e2,e1,e2.
+
+Exact elimination checks every pair of the four left cosets and every
+subblock of one pair. Literal inherited vectors span the computed kernels.
+The fixtures contain both possible overlapping class types, singleton with
+singleton and singleton with triple. Controls separately place a singleton
+inside W, make it parallel to a triple column, duplicate two singleton
+columns, and discard later outputs outside the source. Each alteration
+admits more than two directions on at least one enumerated two-coset block.
+The receipt records the measured dimensions rather than assuming them.
+
+Three or more source cosets can contribute several singleton columns at
+one output, permitting dependencies not excluded by this proof. This paper
+does not decide that case, other triples' subgroups, or arbitrary owner
+sets outside two left cosets. The rank-one-per-observation tariff, physical
+acquisition, native phases, dirty restoration, storage, precision, compiler
+and outer obligations remain separate. No new kappa or complete
+multiplication theorem is claimed.

research/centre-two-coset-separation/README.md

@@ -0,0 +1,107 @@
+# Two translated centre blocks have exactly two hidden directions
+
+For every pair of distinct left cosets of PR3828's 4080-owner subgroup,
+the full scalar common-observation kernel is exactly the two known constant
+triple directions, one per block. Pairing blocks creates no additional
+hidden direction or improvement in information-compression density.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: **scoped algebraic proof with finite corroboration**. This settles
+the two-coset case of Open next question 1 in Clear1nsight's
+[PR3828](https://github.com/CrocSwap/integer-mult-bounds/pull/3828).
+The exact extra-linear-observation minimum on both full blocks is
+`104*8160-2 = 848638`. For any subblock A of their union, the minimum is
+`104|A|-j`, where j counts the complete cosets retained in A.
+
+[PROOF.md](PROOF.md) proves the result for every relative translation,
+without assuming the subgroup is normal. At a later output, each block
+contributes a singleton port or the distinguished triple. Two triple
+contributions cannot meet. Distinct singleton columns cannot cancel each
+other; a singleton also cannot cancel a vector in the triple plane. All
+other ports vanish, leaving the inherited connected triple equations on
+each block separately.
+
+The new source check proves that exactly ports `{0,6,85}` lie in that plane.
+The single-block coset classification and order, reader rank and pairwise
+column independence are cited predecessor premises. Their certificates are
+not reverified. The theorem concerns the historical calls-0/4 scalar model,
+not an automatically applicable replacement for the selected P104 word.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and its standard library suffice.
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/centre-two-coset-separation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/centre-two-coset-separation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/centre-two-coset-separation
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/centre-two-coset-separation --check-source-history
+```
+
+Any CPython 3.12 executable can replace the local interpreter path.
+Expected markers are `PASS_CENTRE_TWO_COSET_SEPARATION`,
+`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`.
+The direct check writes only stdout. Optional `--receipt /absolute/new/path`
+writes a fresh receipt outside the package, binding every package file by
+SHA256. No receipt is handwritten or committed.
+
+Exact source-column elimination checks 109 outside-plane columns. A new
+small S3 times C2 model checks all six two-coset pairs and all 64 subblocks
+of one pair, using literal matrices and kernel witnesses. Four controls
+show why column separation and retaining all later outputs are necessary.
+The proof supplies the universal result; these finite checks corroborate it.
+
+## Scope and credit
+
+The historical source order gives 8160 owners and a derived observation
+minimum of 848638. The large source matrix is not replayed. Source-bound
+metadata orientation passed on canonical main
+`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. The selected
+conditional kappa is `0.003125804` and is unchanged.
+
+Credit Chris R / Clear1nsight PR3828 for the question and full one-block
+classification, Ross Richardson PR3797 for the parallel one-block proof
+and observation interface, Matarener PR3656 for the subgroup and witness,
+Sagar Thakrar PR3291 for the nonparallel-column premises, and Ross
+Richardson PR3071 for the reader/model extraction convention. Retain David
+Charbonneau PR3147, Sudarsh Chaturvedi PR3168, ywz65, Aaron Wang and the
+selected native/geometry/compiler lineage credited by these packages.
+No predecessor credit or frozen file is changed.
+
+No physical collector, recursive tariff, native implementation, improved
+kappa or complete multiplication theorem is supplied. All five selected
+framework assumptions remain. No Lean, Docker, selected cold replay or
+independent human/formal-kernel review is claimed.
+
+## Open next questions
+
+Can three distinct left cosets have extra mixed kernel directions? At one
+output, three singleton columns can be dependent, so the two-coset proof
+ends there. First derive the actual outgoing incidences of one explicit
+three-coset block and its coefficient compatibility. A useful physical
+extension still needs source access, dirty restoration and a complete
+paid/productive invoice; a scalar dimension is not a saved recursive call.
+
+## Implementation constraints
+
+Build the Lever supplies the source-plane checker and exact small-model
+elimination. Prove It Works requires literal matrix kernels and controls
+that break the stated hypotheses. No predecessor verifier is imported.
+
+Power of Ten review: no recursion, dynamic execution or subprocesses;
+source prefix loops have exactly 10851 events times eight rows, and source
+rank tests have eight rows and at most three columns. Small-model systems
+have at most 72 rows and 30 columns. All functions are under 60 lines.
+The source archive is hash-authenticated and bounded before decompression;
+it contains no executable dependency. Receipts refuse existing destinations.
+Explicit checks remain active under optimized Python.
+
+Rule 3 deviation: Python integers, Fraction and JSON/tar libraries allocate
+dynamically. This is a bounded reference verifier, not a fixed-allocation
+runtime. Bounds are eight MB for the authenticated archive, eight MB for
+the decoded word, 704 live covector entries per row and 80-by-30 maximum
+elimination storage. Runtime/library internal allocation is not instrumented.
+The exact archive hash fixes decompression input before library allocation.
+Warning-strict normal/optimized execution and AST parsing provide diagnostics;
+no additional type checker or linter was run.

research/centre-two-coset-separation/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/community-frontier1094-audit/selected-replay.tar.gz",
+      "usage": "input",
+      "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f",
+      "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6"
+    },
+    {
+      "path": "research/centre-sheaf-fibre/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f676ac48edfa05bfe959b4c83f556ab143f736bf",
+      "sha256": "f943dde4863c496020835da7e8d82515635f150a82c3eb4a0666e1ab8509c867"
+    },
+    {
+      "path": "research/centre-sheaf-fibre/README.md",
+      "usage": "provenance",
+      "git_blob": "2c8168eee3c81c2a5c4598aa5629f98158b7d3ba",
+      "sha256": "31a7eedd13fd8abbbef475dba322cec3e30a0ee09b84d5c312c263d9a923057a"
+    },
+    {
+      "path": "research/centre-coset-full-kernel/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f0e5ed2ed570a138ac3d734f51003e97486e4bb6",
+      "sha256": "c929ab00c3c018ced4d2ca776758bd1251f62630fa29f2f6a93c944a5d00c9ca"
+    },
+    {
+      "path": "research/centre-block-moore-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "57e4adae5ab6247d7f82fefc2d91abccdb4bd39a",
+      "sha256": "4ff55b8d7c32f4ad2e32e267fd3e3340003b580dfa709577016eb605f157e137"
+    },
+    {
+      "path": "research/centre-block-coset-kernel/README.md",
+      "usage": "provenance",
+      "git_blob": "f27dc04894b04dfbe60152adb77ac69b5b5f0628",
+      "sha256": "c7594aa840999aa366d834500f0b13cd870c215b321eacdfb0da43bc35d7eef6"
+    }
+  ]
+}