Cambrian Wins
Official registry · machine-authored theorems admitted into Recognition Science
Each entry below is a theorem Cambrian discovered, wrote as a formal proof, and earned into Recognition Science: new mathematics now load-bearing on the permanent theory map. Lean checks every proof. An independent AI judge decides admission. This page lists every result that has passed all four gates; the machine-readable record is wins.json.
What counts here
- 01 · ProofThe Lean kernel accepts the theorem under the allowed axiom set.
- 02 · ProvenanceThe ordinary Cambrian runner authored the result end to end, including its held-out consequence. No hand-written theorems, no hand probes.
- 03 · UseThe result makes a real connection inside Recognition Science and survives a held-out consequence.
- 04 · AdmissionAn independent AI judge reads the theorem in its Recognition Science chapter and returns ACCEPT_CANONICAL.
Admission means the theorem belongs in the theory. It does not establish world-first priority, and it does not replace physical experiment.
The registry
12 admitted results
-
CW-0012 · admitted 2026-07-19
One Wang matrix inverts against its return map
Ask which integer parameters make the Wang matrix multiply its return map to the identity. The solution set has exactly one element. The theorem counts the inverse condition itself across the full integer family.
This is the first direct machine-to-machine compound in the public sequence. Its held-out continuation uses CW-0011 as a load-bearing parent and proves that the Wang-inverse fiber and golden-return fiber have the same size, with no new scaffolding.
Nat.card {k : ℤ // wangMatrix k * returnMap k = 1} = 1Claim boundaryTHEOREM only for the banked algebraic Wang-matrix and return-map family. It does not derive the physical linking number or construct the topological carrier. No new scaffolding was needed. No world-first or priority claim.
-
CW-0011 · admitted 2026-07-19
The golden return-map family has one golden parameter
Ask which integer linking parameters make the algebraic return map satisfy the golden relation. The solution set has exactly one element. The theorem counts the golden predicate over the whole integer family rather than a pre-listed parameter.
Adds a direct cardinality interface to the golden monodromy front-end. Downstream proofs can now use the uniqueness of the golden return-map fiber without rebuilding the subtype transport from the characterization theorem.
Nat.card {k : ℤ // GoldenRelation (returnMap k)} = 1Claim boundaryTHEOREM only for the algebraic family k ↦ returnMap k. It does not derive the physical linking number from the kernel or construct the underlying topology. One new integer singleton scaffold was needed. No world-first or priority claim.
-
CW-0010 · admitted 2026-07-19
Kepler non-precession selects one dimension
Ask which natural dimensions make the closed-form apsidal angle equal one full turn, so an orbit returns without precession. The answer set has exactly one element. The theorem counts the Kepler condition itself rather than a pre-listed dimension.
Adds the Kepler side of dimensional rigidity to the canonical Foundation spine as a counting law. CW-0004 counted the synchronization-minimizing dimensions. This theorem counts the non-precessing dimensions, and the runner's held-out proves those two solution sets have the same size.
Nat.card {D : ℕ // apsidalAngle D = 2 * Real.pi} = 1Claim boundaryTHEOREM for the closed-form apsidal-angle specialization formalized in DraftV1. It does not add the classical-mechanics derivation that precedes that specialization. No new scaffolding was needed. No world-first or priority claim.
-
CW-0009 · admitted 2026-07-19
The 8-by-45 synchronization equation has one solution
Ask which natural dimensions make the least common multiple of 2^D and 45 equal 360. The solution set has exactly one element. The theorem counts the synchronization equation itself rather than a pre-listed answer.
Adds the 8-to-45 hinge to the canonical dimension-forcing spine as a counting law. CW-0007 says the eight-tick equation has one solution. This theorem shows the same uniqueness survives when the gap-45 cycle is folded into the least-common-multiple condition, and the runner's held-out connects the two counts directly.
Nat.card {D : ℕ // Nat.lcm (2 ^ D) 45 = 360} = 1Claim boundaryTHEOREM over the naturals. The equation is formalized exactly as Nat.lcm (2^D) 45 = 360. No new scaffolding was needed because this run reused the D = 3 singleton schema from CW-0004. No world-first or priority claim.
-
CW-0008 · admitted 2026-07-19
The octave unit group has four elements
Among the eight residues of the octave clock, exactly four are invertible: the odd classes 1, 3, 5, and 7. The theorem counts the semantic unit property itself. The explicit odd list is the checked bridge, not the definition of the counted set.
Puts the unit-group count of the octave algebra on the canonical Foundation spine. The four invertible phases form the Klein four-group already used in the chapter, so the count connects the eight-tick clock to its full automorphism structure in one reusable cardinal law.
Nat.card {x : ZMod 8 // IsUnit x} = 4Claim boundaryTHEOREM over the finite ring ZMod 8. The judge found the unit predicate semantically distinct from the explicit odd-residue schema. The held-out is valid but only moderately independent, which lowered confidence to 0.82. No world-first or priority claim.
-
CW-0007 · admitted 2026-07-19
The 8-tick equation has exactly one solution
Ask which spatial dimension counts D satisfy the 8-tick equation, two to the power D equals eight. Over all naturals the solution set has exactly one element. The count is taken over the equation itself, not over a pre-listed answer.
Packages the arithmetic kernel of the 8-tick to three-dimensions hinge (registry item F-003) as a counting law on the canonical Unification surface, beside the T7/T8 guideposts. Together with CW-0004 it gives the dimension-selection story two independent counting forms: one from synchronization minimization, one from the 8-tick equation, both landing on the same singleton.
Nat.card {D : ℕ // 2 ^ D = 8} = 1Claim boundaryTHEOREM over the naturals. The judge noted the bridge to D = 3 is elementary arithmetic, weaker than CW-0004's minimization principle, and granted win credit at 0.78. No new scaffolding: reuses the shared singleton schema parent already counted for CW-0004. No world-first or priority claim.
-
CW-0006 · admitted 2026-07-19
The cell's gauge-fiber count
Fix any configuration of the recognition cell and count the configurations that carry the same boundary record. The answer is exactly 16, for every starting configuration. Gauge classes are cosets of the 16-element record kernel, so every fiber has the kernel's size: what the boundary cannot distinguish is the same 16-fold blindness everywhere in the state space.
Completes the cell's gauge story on the canonical Holography surface: CW-0003 counted the moves invisible from every base; this counts, for each base, the states the record confuses with it. It is the cardinality form of gauge-classes-are-kernel-cosets, the structure the fork selector uses to define physical states. It is also the first theorem minted by the fiber-transport operator, built to close the typed wall this exact statement raised one cycle earlier.
∀ (c : CellCfg), Nat.card {c' : CellCfg // gaugeRel c c'} = 16Claim boundaryTHEOREM over the finite cell model; the coset characterization gauge_iff_kernel is exhaustively checked. No world-first or priority claim. This pair was a typed wall (missing translation-fiber operator) one cycle earlier; the statement became reachable with zero per-target hand work once the generic operator landed.
-
CW-0005 · admitted 2026-07-19
The self-dual coupling dimension is unique
The coupling-dimension duality swaps the two outer dimensions and fixes the middle one. Counting its fixed points over the fixed-point property itself gives exactly one. This uniqueness is the mechanism that forces the colorless lepton sector to the loop dimension in the sector-assignment derivation.
Puts the fixed-point uniqueness of the coupling-dimension duality on the canonical Masses surface in counting form. The sector-dimension derivation forces the lepton to the self-dual dimension precisely because an equivariant bijection must carry the unique conjugation fixed point to the unique duality fixed point; this theorem is that uniqueness as a cardinality law.
Nat.card {d : Fin 3 // dimDual d = d} = 1Claim boundaryTHEOREM over the finite coupling-dimension model (Fin 3). The judge noted the small ambient type lowers novelty strength and the held-out leans on the mint's own scaffold; win credit was granted at 0.74 confidence because the counted predicate (involution fixed point) is semantically distinct from the literal index. No world-first or priority claim.
-
CW-0004 · admitted 2026-07-19
Sync-minimization selects exactly one dimension
Among all possible spatial dimension counts, ask which ones are admissible (at least three) and minimize the recognition synchronization period. The answer set has exactly one element. The count is taken over the semantic minimization property across ALL naturals, not over a pre-listed answer.
Packages dimensional rigidity as a single counting law on the canonical surface: the (S) synchronization constraint of the dimensional-rigidity paper does not merely imply D = 3, its solution set is literally a one-element set. This is the counting form of why reality has three spatial dimensions, sitting beside the T8 guidepost on the Skeleton spine.
Nat.card {D : ℕ // ConstraintS D} = 1Claim boundaryTHEOREM over the formalized (S) constraint (admissibility plus syncPeriod minimization as defined in the Lean paper surface). No world-first or priority claim.
-
CW-0003 · admitted 2026-07-19
The cell's silent-move count
A move applied to a recognition cell is silent when it leaves the boundary record unchanged from every possible starting configuration. Exactly 16 of the cell's 256 moves are silent. The count is taken over the semantic property itself (invisible from every base), not over a pre-defined list of kernel elements.
Puts the whole-cell blindness law on the canonical Holography surface in its semantic form: what a boundary record can never see is a 16-element group of cell-global moves. The held-out consequence equates this silent-move count with the posted-record image count, exhibiting the rank-nullity balance of the cell record map as a single cardinality equation.
Nat.card {d : CellCfg // ∀ c : CellCfg, faceRecord (xorCfg c d) = faceRecord c} = 16Claim boundaryTHEOREM over the finite cell model; the bridge from universal invisibility to the kernel is the exhaustively checked invisible_iff_kernel. No world-first or priority claim. A sibling candidate from the same session (the glued-pair kernel count) was denied by the same judge as thin packaging and stays quarantined; this entry cleared that bar because the counted predicate is not the kernel's definition.
-
CW-0002 · admitted 2026-07-19
The 2D affine-sector count
Count the configurations of a two-dimensional M×N recognition grid that are affine: built from whole-row and whole-column flips over a base value. The answer is exactly 2^(M+N+1), a perimeter law. These are precisely the configurations a boundary record cannot see, counted directly over their structural description rather than through the kernel of the record map.
Exposes the D=2 perimeter law in its structural form on the canonical Holography surface: the grid's record-invisible sector, described as affine configurations, has a count that grows with the perimeter and not the area. The held-out consequence ties this 2D count to the D=3 closed-sector count of the cube law (CW-0001) in one equality, connecting the dimension story the chapter tells.
∀ (M N : ℕ), Nat.card {x : CornerCfg M N // IsAffine M N x} = 2 ^ (M + N + 1)Claim boundaryTHEOREM for the stated shared-vertex lattice model; inherits that named conditionality. No world-first or priority claim. The judge framed this as canonical lemma utility, smaller in scope than CW-0001; no scaffolding parent was needed, and the statement and its held-out consequence were authored end to end by the ordinary runner.
-
CW-0001 · admitted 2026-07-19
The D=3 cube nullity law
Count the configurations of a three-dimensional M×N×P recognition block whose face records are closed. The answer is exactly 2^(M+N+P+1): an edge law, growing with the sides rather than the faces or the volume. The record-invisible share of the bulk vanishes even faster in three dimensions than in two.
Closes the named open cube-nullity target in the Recognition Holography chapter. Together with the 2D perimeter law and the flat-cube collapse bridge, it completes the kernel-cardinality story across dimensions: what a boundary record cannot see is a vanishing sliver, in every dimension checked.
∀ (M N P : ℕ), Nat.card {x : CubeCfg M N P // IsClosed M N P x} = 2 ^ (M + N + P + 1)Claim boundaryTHEOREM for the stated shared-vertex lattice model; inherits that named conditionality. No world-first or priority claim. The counting scaffolding parent was hand-built; the winning statement and its held-out consequence were authored by the ordinary runner.