Cambrian Wins
Official registry · machine-authored theorems admitted into Recognition Science
Every entry on this page is a theorem a machine found. Cambrian composed the claim, wrote the proof, and earned its place in Recognition Science: new mathematics that now carries weight on the permanent map. The Lean kernel checked every line before it counted, and an independent judge decided whether it belongs. This page lists every result that cleared 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 · ProvenanceCambrian authored the result end to end. No human wrote a theorem or a proof; where the protocol allowed a correction pass, the entry says so.
- 03 · UseThe result makes a real connection inside Recognition Science and survives its held-out or causal checks: delete a load-bearing parent and the proof has to die.
- 04 · AdmissionAn independent AI judge reads the theorem in its Recognition Science chapter and returns ACCEPT_CANONICAL. The newest entries required two, from different model families.
Admission means the theorem belongs in the theory. It does not establish world-first priority, and it does not replace physical experiment.
The registry
52 admitted results
-
CW-0052 · admitted 2026-07-24
Almost-least phantom rates keep nearby log ceilings
Any two eps-almost-least phantom rates have log-ceilings differing by at most the logarithmic diameter of the rate-ceiling map on the almost-least interval. Near-least rates cannot scatter their ceilings freely.
W1 Reproducer kill-test slot WR33. It upgrades the exact least-phantom-rate ceiling identity into a quantitative two-rate stability law around that forced arcosh pin.
|Real.log (kappa / (2 * (1 - q1))) - Real.log (kappa / (2 * (1 - q2)))| ≤ phantomRateCeilingGap kappa c eps ∧ |Real.log (kappa / (2 * (1 - q1))) - Real.arcosh (1 + c)| ≤ phantomRateCeilingGap kappa c eps ∧ |Real.log (kappa / (2 * (1 - q2))) - Real.arcosh (1 + c)| ≤ phantomRateCeilingGap kappa c epsClaim boundaryTHEOREM for AlmostLeastPhantomRate pairs under the stated kappa and eps strip: log-ceilings differ by at most the rate-ceiling diameter on that interval. The load-bearing parent is exact_ratioBridge_deficit_ceiling_via_least_phantom_rate. No world-first or priority claim.
-
CW-0051 · admitted 2026-07-24
Near-best J points keep a bounded ratio cost
The ratio of any two positive eps-approximate global minimizers of J has J-cost at most twice eps times (eps plus 2). Approximate minimizers cannot form an arbitrarily costly ratio.
W1 Reproducer kill-test slot WR21. It upgrades unique-minimum forcing of J into a quantitative two-object composition rate on approximate minimizers.
J (x / y) ≤ 2 * eps * (eps + 2)Claim boundaryTHEOREM for positive eps-approximate global minimizers of J: J(x/y) ≤ 2*eps*(eps+2). The load-bearing parent is J_unique_minimum. No world-first or priority claim.
-
CW-0050 · admitted 2026-07-24
Separated almost-least periods pay a quadratic deficit
If two times are almost-least deficit periods for a local horizon context, then the square of their separation, scaled by kappa squared over pi squared, is at most the sum of their deficit costs. Separation forces quadratic cost.
W1 Reproducer kill-test slot WR18. It upgrades exact least-period pinning into a reverse quadratic stability rate for the almost-least cluster.
(kappa ^ 2 / Real.pi ^ 2) * (T - S) ^ 2 ≤ deficitCost (kappa * T) + deficitCost (kappa * S)Claim boundaryTHEOREM for AlmostLeastDeficitPeriod pairs in a LocalHorizonContext: (kappa^2/pi^2)*(T-S)^2 is at most the sum of deficit costs. The load-bearing parent is euclideanPeriod_isLeast_for_context. No world-first or priority claim.
-
CW-0049 · admitted 2026-07-24
Near-best J-cost points on a hard wall stay close
On a convex feasible set supported above 2 that contains the wall point 2, any two eps-approximate J-cost minimizers differ by at most (8/3)*eps. The slope of J-cost at the forced endpoint sets the constant.
W1 Reproducer kill-test slot WR27. It upgrades unique-minimizer forcing into an explicit linear diameter for the eps-relaxed minimality predicate on boundary-supported feasible sets.
|x - y| ≤ (8 / 3 : ℝ) * epsClaim boundaryTHEOREM for convex feasible sets in [2,∞) containing 2: eps-approximate J-cost minimizers have diameter at most (8/3)*eps. The load-bearing parent is unique_minimizer_principle. No world-first or priority claim.
-
CW-0048 · admitted 2026-07-24
Different factorization weights keep a cosh-controlled gap
Two factorization-forced lifts through distinct weight vectors have evaluation gap controlled by cosh of the aggregate bound times the log-aggregate gap, plus a shell from any eps slack. Distinct weights cannot hide an unbounded silent gap.
W1 Reproducer kill-test slot WR26. It upgrades exact factorization forcing into a two-object quantitative law across distinct weight vectors.
|F x - H x| ≤ cosh M * epsClaim boundaryTHEOREM for factorization-forced lifts through weight vectors α and β: the evaluation gap is controlled by a cosh(M) envelope times the log-aggregate gap. The load-bearing parent is forced_of_factorization. No world-first or priority claim.
-
CW-0047 · admitted 2026-07-24
Near-cosine initial data keep nearby angle oscillators
Two twice-smooth solutions of the angle oscillator ODE whose initial values and derivatives sit within eps of the forced (1, 0) data remain within (|cos| plus |sin|) times twice eps of each other at every time.
W1 Reproducer kill-test slot WR24. It turns exact cosine uniqueness into a sharp two-object stability law under eps-relaxed initial data on the recognition-angle surface.
∀ t, |H t - F t| ≤ 2 * ε * (|Real.cos t| + |Real.sin t|)Claim boundaryTHEOREM for ContDiff-2 solutions of f'' = -f with initial data within eps of (1,0): pointwise gap is controlled by 2*(|cos t| + |sin t|)*eps. The load-bearing parent is ode_cos_uniqueness. No world-first or priority claim.
-
CW-0046 · admitted 2026-07-24
Approximate positive golden roots stay slope-close
Above the positive root of x squared equals x plus one, any two eps-approximate roots differ by at most eps over twice the root minus one. The residual slope of the golden polynomial controls the cluster width.
W1 Reproducer kill-test slot WR25. It upgrades unique positive-root forcing into an explicit slope-modulus diameter on the half-line above the root.
|x - y| ≤ eps / (2 * r - 1)Claim boundaryTHEOREM for the positive root of x^2 = x + 1 and eps-approximate roots at least that root: diameter is at most eps/(2*r - 1). The load-bearing parent is phi_unique_pos_root. No world-first or priority claim.
-
CW-0045 · admitted 2026-07-24
Near-hom chords keep a bounded Born-defect diameter
In a CP6 referring algebra, any two neutral unit chords that sit within eps of the unique structure-preserving image of a referring trace have Born defect at most four times eps. Near-hom chords form a controlled cluster.
W1 Reproducer kill-test slot WR23. It upgrades unique homomorphism forcing into a quantitative two-chord Born-defect diameter on the Light Language geometry surface.
bornDefect ψ.chord φ.chord ≤ (4 : ℝ) * epsClaim boundaryTHEOREM for eps-near-value chords of the unique hom into a CP6 target algebra (eps at most 1/2): Born-defect diameter is at most 4*eps. The load-bearing parent is unique_hom_into_target_algebra. No world-first or priority claim.
-
CW-0044 · admitted 2026-07-24
Forced scale costs obey a half-rate cross gap
After reciprocal normalized cost collapse names a unique positive scaleCost, any two eps-lifts satisfy a cross gap of at most twice eps plus half the powered-argument gap times the reciprocal factor. The half-rate term can grow without an a-priori ceiling.
W1 Reproducer kill-test slot WR08. It adds the sharp reciprocal half pair-gap rate on the forced powered arguments, with unique scaleCost collapse as the load-bearing parent.
ℝ, 0 < lam ∧ (∀ t : ℝ, 0 < t → F t = scaleCost lam t) ∧ |A x - B y| ≤ (2 : ℝ) * eps + (1 / 2 : ℝ) * |positivePowerMap lam x - positivePowerMap lam y| * (1 + (positivePowerMap lam x * positivePowerMap lam y)⁻¹)Claim boundaryTHEOREM for reciprocal normalized continuous costs with positive second derivative at the collapse: eps-lifts obey the half-rate cross gap through the forced scaleCost parameter. The load-bearing parent is the unique scaleCost collapse theorem. No world-first or priority claim.
-
CW-0043 · admitted 2026-07-24
Near-constant credits keep a controlled log-partition gap
Two eps-near-constant credit fields on a finite full-support probability space have log-partition gap bounded by the gap of the parent-forced single-mode greatest values plus twice the oscillation tolerance.
W1 Reproducer kill-test slot WR11. It upgrades single-mode reduction forcing into a quantitative two-credit stability law through the forced greatest values.
|logPartition p X - logPartition p Y| ≤ |g_u - g_v| + (2 : ℝ) * εClaim boundaryTHEOREM for eps-near-constant credits under full-support probability: the log-partition gap is at most the forced greatest-value gap plus 2*eps. The load-bearing parent is singleMode_reduction. No world-first or priority claim.
-
CW-0042 · admitted 2026-07-24
Near-link positives keep J-cost strictly below one half
When two positive numbers sit within eps less than 1 of the forced critical link against phi, each ratio to the forced witness has J-cost strictly below one half. The golden-square threshold is a hard ceiling inside that approximate solution set.
W1 Reproducer kill-test slot WR05. It upgrades unique positive-link forcing into a sharp J-cost threshold on the whole eps-approximate positive solution set.
∃ u₀ : ℝ, (0 < u₀ ∧ u₀ * theta_crit = phi) ∧ Jcost (x / u₀) < (1 : ℝ) / 2 ∧ Jcost (y / u₀) < (1 : ℝ) / 2Claim boundaryTHEOREM for positive x, y with |x*theta_crit - phi| ≤ eps < 1: both Jcost(x/u0) and Jcost(y/u0) are strictly below 1/2 at the forced positive witness u0. The load-bearing parent is anthropic_principle_inapplicable. No world-first or priority claim.
-
CW-0041 · admitted 2026-07-24
A unit probe gap controls the double-probe cost gap
Once the forced scale gap is controlled by the exp(1) probe, the cost gap at exp(2) on the compact scale band from 1 to 2 is controlled by an explicit multiple of that same probe gap. The unit probe transports to the double probe.
W1 Reproducer kill-test slot WR02S, deepening WR02. It adds a probe-to-cost transport law on [1,2] with the WR02 stability theorem as load-bearing parent.
∃ (lamF lamG : {lam : ℝ // 0 < lam}), (∀ x : ℝ, 0 < x → F x = scaleCost lamF x) ∧ (∀ x : ℝ, 0 < x → G x = scaleCost lamG x) ∧ |F (exp 2) - G (exp 2)| ≤ (4 * cosh 2 * cosh (1 / 2)) * epsClaim boundaryTHEOREM for continuous nonflat positive extensions on scale band [1,2]: the exp(2) cost gap is controlled by the exp(1) probe gap with factor 4*cosh(2)*cosh(1/2). The load-bearing parent is continuous_positive_extension_probe_stability. No world-first or priority claim.
-
CW-0040 · admitted 2026-07-24
Near-cosh initial data keep nearby ODE solutions
Two twice-smooth solutions of the hyperbolic oscillator ODE whose initial values and derivatives sit within eps of the forced (1, 0) data remain within twice (cosh plus absolute sinh) times eps of each other at every time.
W1 Reproducer kill-test slot WR14. It turns exact cosh uniqueness into a sharp two-object stability law under eps-relaxed initial data.
∀ t, |H t - F t| ≤ 2 * ε * (cosh t + |sinh t|)Claim boundaryTHEOREM for ContDiff-2 solutions of f'' = f with initial data within eps of (1,0): pointwise gap is at most 2*(cosh|t| + |sinh t|)*eps. The load-bearing parent is ode_cosh_uniqueness. No world-first or priority claim.
-
CW-0039 · admitted 2026-07-24
Near-zero balance residuals pin nearby positive scales
Any two positive scales whose balance residual is at most eps in absolute value differ by at most a fixed stability constant times eps. Near-zeros of the balance equation form a linear cluster on the positive ray.
W1 Reproducer kill-test slot WR13. It upgrades unique positive-root forcing of the balance residual into a quantitative two-object modulus.
|x - y| ≤ balanceResidualStabilityConst * epsClaim boundaryTHEOREM for positive scales with |balanceResidual| ≤ eps: |x - y| ≤ balanceResidualStabilityConst * eps. The load-bearing parent is balance_unique_positive_root. No world-first or priority claim.
-
CW-0038 · admitted 2026-07-24
Consecutive active edges stay at least almost one apart
Across successive ticks, eps-near coordinates of the unique active cube-bits cannot collapse closer than one minus twice eps. Successive forced edges keep a structure-derived separation rather than an ambient diameter ceiling.
W1 Reproducer kill-test slot WR03. It turns unique-edge-per-tick forcing into a quantitative multi-tick separation law the parent never states.
(1 : ℝ) - (2 : ℝ) * ε ≤ |a - b|Claim boundaryTHEOREM for eps-near abstract coordinates of successive unique active edges: |a - b| is at least 1 - 2*eps. The load-bearing parent is unique_edge_per_tick. No world-first or priority claim.
-
CW-0037 · admitted 2026-07-24
Near-CODATA corrected loads stay within a linear band
If two loads make the corrected dressing hit within eps of the CODATA inverse-alpha value, then the loads themselves differ by at most a fixed residual-stability constant times eps. Near-hits force nearby loads.
W1 Reproducer kill-test slot WR01. It upgrades the exact CODATA-equality pin into a quantitative residual modulus on the whole real load line.
|x - y| ≤ residualStabilityConst * epsClaim boundaryTHEOREM for loads with |correctedAlphaInv - alpha_inv_CODATA| ≤ eps (eps at most half the anchor): |x - y| ≤ residualStabilityConst * eps. The load-bearing parent is corrected_eq_codata_iff. No world-first or priority claim.
-
CW-0036 · admitted 2026-07-24
Near-least deficit-free periods form a tight pair
In the half-turn window, any two positive times whose deficit costs are at most eps and that sit above the Euclidean phase floor differ by at most arccos(1 - eps) over kappa. Near-least deficit-free periods cannot wander farther than that explicit width.
W1 Reproducer kill-test slot WR12. It upgrades exact leastness of the Euclidean period into a sharp two-object diameter for the eps-near deficit-free cluster.
|T - S| ≤ Real.arccos (1 - eps) / kappaClaim boundaryTHEOREM for positive times with deficitCost(kappa*T) ≤ eps above the half-turn floor: pair diameter is at most arccos(1-eps)/kappa. The load-bearing parent is euclideanPeriod_isLeast. No world-first or priority claim.
-
CW-0035 · admitted 2026-07-24
Near-CODATA closing loads stay linearly close
If two loads make the corrected inverse-alpha dressing land within eps of the CODATA anchor, then those loads differ by at most a fixed multiple of eps. The constant is built from the anchor and the dressing slope.
W1 Reproducer kill-test slot WR07. It turns unique closing-load existence into a quantitative two-object Lipschitz law on the unbounded load line.
|x - y| ≤ stabilityConst * epsClaim boundaryTHEOREM for loads whose corrected dressing is within eps of alpha_inv_CODATA (with eps below half the anchor): |x - y| is at most stabilityConst * eps. The load-bearing parent is existsUnique_closingLoad. No world-first or priority claim.
-
CW-0034 · admitted 2026-07-24
Near-factorizations keep a half-rate evaluation gap
When two lifts stay within eps of J-cost on the same aggregate, their cross evaluation gap is at most twice eps plus half the aggregate gap times the usual reciprocal factor. Approximate factoring still inherits the sharp half-rate identity.
W1 Reproducer kill-test slot WR31. It relaxes exact factorization while keeping scalar forcing, and adds an explicit cross-evaluation rate the uniqueness parent never states.
|F x - H y| ≤ (2 : ℝ) * eps + (1 / 2 : ℝ) * |aggregate α x - aggregate α y| * (1 + (aggregate α x * aggregate α y)⁻¹)Claim boundaryTHEOREM for eps-approximate factorizations through a common aggregate with exact scalar J-cost forcing: the cross evaluation gap obeys the half-rate bound plus a 2*eps shell. The load-bearing parent is forced_of_scalar_uniqueness. No world-first or priority claim.
-
CW-0033 · admitted 2026-07-24
Close cost probes force close positive scales
Two continuous positive cost extensions that stay within eps at the exp(1) probe must have forced positive scales within an explicit multiple of that probe gap. The comparison uses the closed-form factor sinh(1) on the unbounded scale ray.
W1 Reproducer kill-test slot WR02. It upgrades unique positive-scale collapse into a two-object Lipschitz stability law at a fixed probe, with the parent load-bearing for naming the scales.
∃ (lamF lamG : {lam : ℝ // 0 < lam}), (∀ x : ℝ, 0 < x → F x = scaleCost lamF x) ∧ (∀ x : ℝ, 0 < x → G x = scaleCost lamG x) ∧ |lamF.val - lamG.val| * sinh 1 ≤ epsClaim boundaryTHEOREM for continuous nonflat positive extensions: the forced scale gap is controlled by the exp(1) probe gap with factor involving sinh(1). The load-bearing parent is continuous_reciprocal_normalized_rcl_nonflat_unique_positive_scale. No world-first or priority claim.
-
CW-0032 · admitted 2026-07-23
Near-best sourced hinge paths stay pointwise close
Grant a global minimizer of the sourced hinge action. Any two configurations that come within eps of that minimum stay within twice the square root of twice eps at every tick.
Seventh unified-loop landing and first offspring of the re-rooted sourced unique-minimizer tip on gravity lineage LG1. It upgrades uniqueness of the sourced well into a pointwise diameter for approximate minimizers.
|u i - v i| ≤ 2 * Real.sqrt (2 * eps)Claim boundaryTHEOREM for the sourced hinge action: any global minimizer and any pair of eps-approximate minimizers satisfy a pointwise diameter of 2*sqrt(2*eps). The load-bearing parent is sourced_unique_minimizer. No world-first or priority claim.
-
CW-0031 · admitted 2026-07-23
Approximate golden roots cannot sit far apart
Once a positive root of x squared equals x plus one is named, any two numbers at least 1 whose golden residuals are at most eps differ by at most twice eps over that root. Near-roots form a tight cluster.
Sixth unified-loop landing and first offspring of the re-rooted phi exclusivity tip on lineage LC2. It turns model-independent naming of the golden root into a quantitative diameter for approximate roots.
|x - y| ≤ 2 * eps / rClaim boundaryTHEOREM for the positive root of x^2 = x + 1 and eps-approximate roots at least 1: diameter is at most 2*eps/r. The load-bearing parent is exclusivity_model_independent. No world-first or priority claim.
-
CW-0030 · admitted 2026-07-23
Forced costs on a bounded interval stay Lipschitz
Every primitive cost forced to the closed-form kernel is Lipschitz on the interval from 1 to X. The sharp constant is half of one minus one over X squared, so the slope cannot exceed that geometric ceiling.
Fifth unified-loop landing and first offspring of the re-rooted cost uniqueness tip on lineage L0. It converts exact kernel uniqueness into an explicit two-point Lipschitz law on bounded positive intervals.
|F x - F y| ≤ ((1 - 1 / X ^ 2) / 2) * |x - y|Claim boundaryTHEOREM for primitive-cost class members with the Aczel regularity kernel on [1, X]: |F x - F y| is at most ((1 - 1/X^2)/2) * |x - y|. The load-bearing parent is primitive_to_uniqueness_of_kernel. No world-first or priority claim.
-
CW-0029 · admitted 2026-07-23
Seed-edge depth gaps pin Born sector scores
Build seed-edge signals from an abstract seed measure, then score them with any mode-local Born measure. Whenever two edges differ in depth by at most k, every sector score gap is bounded by the same golden window one minus one over phi to the k.
First earned cross of the unified loop: constants seed Lipschitz and quantum Born forcing as two load-bearing parents from different lineages. It yields a live sector pin neither parent states alone.
∀ S : Finset (Fin 8), |nu (seedEdgeSignal (mu e)) S - nu (seedEdgeSignal (mu f)) S| ≤ 1 - (1 / Constants.phi) ^ kClaim boundaryTHEOREM for the cross of SeedMeasureSpec and mode-local Born class members on seed-edge signals: every sector obeys the golden depth-gap pin. Both parents are load-bearing. No world-first or priority claim.
-
CW-0028 · admitted 2026-07-23
Near-best recognition angles stay cosine-close
Any two angles in the open half-turn that nearly minimize recognition cost on cosines have cosines within the square root of twice the slack. Approximate minimizers cannot wander far in cosine space.
Third unified-loop landing and first offspring of the re-rooted recognition-angle tip on the quantum measurement lineage. It upgrades exact uniqueness of the recognition angle into a diameter law for near-critical angles.
|Real.cos θ₁ - Real.cos θ₂| ≤ Real.sqrt (2 * ε)Claim boundaryTHEOREM for angles in (0, pi) that are eps-near minimizers of R_cost on cosines: cosine diameter is at most sqrt(2*eps). The load-bearing parent is recognition_angle_exists_unique. No world-first or priority claim.
-
CW-0027 · admitted 2026-07-23
Seed measures change at most by a golden depth gap
On any abstract seed-measure pinned by the class-forcing parent, two edges whose depths differ by at most k have measures that differ by at most one minus one over phi to the k. Deeper gaps can open a larger window, but never beyond that golden geometric bound.
Second unified-loop landing and first offspring of the re-rooted constants seed-measure tip. It shows the grant-then-quantify template transfers from quantum Born forcing into the constants lineage.
|mu e - mu f| ≤ 1 - (1 / Constants.phi) ^ kClaim boundaryTHEOREM for SeedMeasureSpec members: edge measures obey the golden Lipschitz bound 1 - (1/phi)^k across depth gaps at most k. The load-bearing parent is seedMeasureSpec_forced. No world-first or priority claim.
-
CW-0026 · admitted 2026-07-23
Nearby signals keep nearby Born sector scores
Take any mode-local measure that is forced to the Born sector rule. If two normalized signals have modulus profiles close in total variation, then their scores on every sector differ by at most twice that closeness.
First accepted offspring of the unified-loop quantum lineage after the LQ2 re-root, and the first assembler landing of that loop. It turns exact Born forcing into a quantitative two-signal stability law the parent never states.
∀ S : Finset (Fin 8), |mu f S - mu g S| ≤ 2 * εClaim boundaryTHEOREM for mode-local Born class members on normalized eight-mode signals: sector scores move by at most twice the l1 modulus gap. The load-bearing parent is modeLocal_born_unique. No world-first or priority claim.
-
CW-0025 · admitted 2026-07-22
Equal-step drops of the corrected dressing strictly shrink
Advance the corrected inverse-alpha dressing by equal positive steps. The drop across the second step is strictly smaller than the drop across the first. Successive equal increments lose less and less under the nonlinear dressing.
First accepted offspring of the constants nonlinear-dressing lineage after re-roots. It turns strict antitonicity of the corrected dressing into a second-difference curvature law: equal-step drops diminish by the rpow factor, a fact bare antitonicity does not give.
correctedAlphaInv (ℓ + h) - correctedAlphaInv (ℓ + 2 * h) < correctedAlphaInv ℓ - correctedAlphaInv (ℓ + h)Claim boundaryTHEOREM for the formalized corrected inverse-alpha dressing with positive equal step h. The load-bearing parent is corrected_strictAnti. No world-first or priority claim.
-
CW-0024 · admitted 2026-07-22
Time-kernel climb is at least n times the first time-mesh gap
On a geometric time mesh for the unclamped ILG time kernel, the total climb from the base time to the n-th mesh point is at least n times the first-step gap. Later time steps cannot undercut that first gap under the kernel's power-law structure.
First landing of the re-rooted gravity time-kernel lineage. It converts strict monotonicity of the time kernel into a uniform geometric time-mesh gap-floor law on the Gravity surface, parallel to the radial enhancement floor of CW-0017.
(n : ℝ) * (w_t P (T0 * ρ) τ0 - w_t P T0 τ0) ≤ w_t P (T0 * ρ ^ n) τ0 - w_t P T0 τ0Claim boundaryTHEOREM for the formalized unclamped ILG time kernel on a geometric time mesh with positive τ0, alpha, Clag, and ρ > 1 inside the unclamped strip. No world-first or priority claim.
-
CW-0023 · admitted 2026-07-22
Enhancement surplus over path-action drop beats the first mesh step
After the corridor-selected junction fires, the surplus of enhancement climb over path-action drop is strictly larger than the first geometric mesh step gap. The comparison is no longer only qualitative: there is an explicit positive margin.
Depth 4 of the quantum lineage, deepening the first earned junction. It stands on the corridor-threshold dominance theorem as a load-bearing Cambrian parent and upgrades drop < climb into a quantitative first-step surplus.
firstStepGap R0 r0 α ρ < w_real (R0 * ρ ^ meshThresholdBlocks R0 r0 α ρ (corridorLeftCeiling n rots)) r0 α - w_real R0 r0 α - (pathAction (pathFromRotation (rots 0)) - pathAction (pathFromRotation (rots n)))Claim boundaryTHEOREM for the formalized corridor-selected enhancement surplus with free R0, r0, α, ρ, n, and rotation mesh. The depth-3 junction parent is load-bearing. No world-first or priority claim.
-
CW-0022 · admitted 2026-07-22
Path-action drop stays below corridor-selected enhancement climb
Feed the measurement corridor's left-endpoint ceiling into the gravity mesh as the crossing target. At the resulting Archimedean index, the ILG enhancement climb strictly exceeds the recognition path-action drop on that same mesh. Neither side alone states the comparison.
The first earned cross-lineage junction of the forest campaign: quantum depth-2 tip and gravity depth-2 leaf as two load-bearing parents from different lineages. Both omit arms fail. It yields a live budget law neither lineage had on its own.
pathAction (pathFromRotation (rots 0)) - pathAction (pathFromRotation (rots n)) < w_real (R0 * ρ ^ meshThresholdBlocks R0 r0 α ρ (corridorLeftCeiling n rots)) r0 α - w_real R0 r0 αClaim boundaryTHEOREM for the formalized cross of the measurement cot sandwich and the ILG mesh threshold crossing, with free R0, r0, α, ρ, n, and rotation mesh. Both parents are load-bearing. No world-first or priority claim.
-
CW-0021 · admitted 2026-07-22
Enhancement climb crosses any nonnegative target
Fix any nonnegative target M on the real ILG enhancement weight. There is an explicit geometric-mesh block count, one past the Archimedean ceiling of M over the first-step gap, at which the climb from the base radius strictly exceeds M.
Depth 2 of the gravity enhancement lineage. It stands on the mesh gap-floor theorem as a load-bearing Cambrian parent and turns that floor into a threshold-crossing index, the gravity arm of the first earned junction.
M < w_real (R0 * ρ ^ meshThresholdBlocks R0 r0 α ρ M) r0 α - w_real R0 r0 αClaim boundaryTHEOREM for the formalized real ILG enhancement weight with nonnegative target M and geometric mesh parameters R0, r0, α, ρ > 1. The depth-1 gap-floor parent is load-bearing. No world-first or priority claim.
-
CW-0020 · admitted 2026-07-22
The path-action drop sits between two cot Riemann sums
On a strictly increasing rotation mesh, the path-action drop is trapped between two cotangent Riemann sums: above the right-endpoint sum and below the left-endpoint sum. The drop has a two-sided corridor, not only a one-sided floor.
Depth 2 of the quantum lineage. It stands on the right-endpoint cot-margin theorem as a load-bearing Cambrian parent and adds the left-endpoint ceiling, giving the corridor wall later used by the first cross-lineage junction.
2 * ∑ k ∈ Finset.range n, ((rots (k + 1)).θ_s - (rots k).θ_s) * Real.cot (rots (k + 1)).θ_s < pathAction (pathFromRotation (rots 0)) - pathAction (pathFromRotation (rots n)) ∧ pathAction (pathFromRotation (rots 0)) - pathAction (pathFromRotation (rots n)) < 2 * ∑ k ∈ Finset.range n, ((rots (k + 1)).θ_s - (rots k).θ_s) * Real.cot (rots k).θ_sClaim boundaryTHEOREM for the formalized two-branch rotation mesh with strictly increasing θ_s. The depth-1 cot-margin parent is load-bearing. No world-first or priority claim.
-
CW-0019 · admitted 2026-07-22
Two near-extremum scales cannot outrun the residual
Take any two positive scales whose curvature residuals are each at most ε. Relative to any exact extremizer μ, those two scales cannot be farther apart than ε over μ. Nearness to the same target forces a diameter bound between the approximants.
First forest lineage to reach depth 2. It stands on the residual-stability law as a load-bearing Cambrian parent: remove that parent and the diameter proof dies. The constants lineage now compounds a stability fact into a two-point diameter law.
∀ μ : ℝ, 0 < μ → J_curv μ = J_bit_val → |lam₁ - lam₂| ≤ ε / μClaim boundaryTHEOREM for two positive residual-near scales in the Planck-scale matching model. The depth-1 residual-stability parent is load-bearing: the omission arm fails without it. No world-first or priority claim.
-
CW-0018 · admitted 2026-07-22
Near-extremum scales stay inside a residual ball
If a positive scale's curvature residual is at most ε from the bit-value target, then every exact extremizer μ sits within ε over twice the sum of the two scales. Closeness in residual forces closeness in scale, with an explicit denominator.
First depth-1 landing of the constants extremum lineage. It turns uniqueness of the Planck-scale curvature extremizer into a quantitative residual-to-distance stability law on the Constants surface.
∀ μ : ℝ, 0 < μ → J_curv μ = J_bit_val → |lam - μ| ≤ ε / (2 * (lam + μ))Claim boundaryTHEOREM for the formalized Planck-scale curvature matching model with nonnegative residual ε and positive scales. No world-first or priority claim.
-
CW-0017 · admitted 2026-07-21
Geometric mesh climb is at least n times the first gap
On a geometric radial mesh for the real ILG enhancement weight, the total climb from the base radius to the n-th mesh point is at least n times the first-step gap. Later steps cannot shrink below that first gap, so the n-fold sum floors the climb.
First depth-1 landing of the gravity enhancement lineage. It converts strict monotonicity of the real enhancement weight into a uniform mesh gap-floor law, the surface later threshold and junction theorems stand on.
(n : ℝ) * (w_real (R0 * ρ) r0 α - w_real R0 r0 α) ≤ w_real (R0 * ρ ^ n) r0 α - w_real R0 r0 αClaim boundaryTHEOREM for the formalized real ILG enhancement weight on a geometric radial mesh with positive R0, r0, α and ρ > 1. No world-first or priority claim.
-
CW-0016 · admitted 2026-07-21
The path-action drop beats its right-endpoint cot floor
Take a strictly increasing mesh of two-branch recognition rotations. The drop in path action from the first angle to the last is strictly larger than twice the right-endpoint cotangent Riemann sum of the angle steps. The floor uses each step's later angle, so every block contributes a positive margin.
First forest landing outside the golden-fold family, rooted in the quantum measurement lineage. It turns the single-step cot margin into an n-step mesh law on the canonical Measurement surface, under the same frozen dual-judge protocol as the earlier breeder wins.
pathAction (pathFromRotation (rots 0)) - pathAction (pathFromRotation (rots n)) > 2 * ∑ k ∈ Finset.range n, ((rots (k + 1)).θ_s - (rots k).θ_s) * Real.cot (rots (k + 1)).θ_sClaim boundaryTHEOREM for the formalized two-branch rotation mesh with strictly increasing θ_s. The load-bearing parent is the measurement bridge identity used as the lineage root. No world-first or priority claim.
-
CW-0015 · admitted 2026-07-20
The golden fold has the strictly smallest exact rate
Recognition growth comes in folds, and every integer fold sets its own J-cost budget. Compare exact least contraction rates across those budgets. The golden fold's rate is strictly smallest: any uniform factor that survives a higher integer-fold budget is strictly larger than the golden fold's exact least rate.
The first Cambrian theorem that stands on another Cambrian theorem as a load-bearing parent under the frozen breeder protocol. Remove the generation-one exact-rate law and this proof dies; the omission arm checks exactly that. It turns the mass-fold cost ordering into a strict rate law and lands the phantom-coupling story on the golden ratio.
IsLeast {q : ℝ | ∀ r : ℝ, 1 / 2 ≤ r → Cost.Jcost r ≤ foldCost 1 → |phiCouplingNewRatio kappa r - 1| ≤ q * |r - 1|} (1 - kappa / (2 * Cost.jcostSublevelHi (foldCost 1))) ∧ ∀ q : ℝ, (∀ r : ℝ, 1 / 2 ≤ r → Cost.Jcost r ≤ foldCost k → |phiCouplingNewRatio kappa r - 1| ≤ q * |r - 1|) → 1 - kappa / (2 * Cost.jcostSublevelHi (foldCost 1)) < qClaim boundaryTHEOREM for the formalized fold-budget model with kappa in (0,1] and integer folds k ≥ 2. Generation one is load-bearing: the omission arm fails without it. One correction pass was used and disclosed. No world-first or priority claim.
-
CW-0014 · admitted 2026-07-20
The exact best contraction rate on a cost budget
Put phantom coupling on a J-cost budget and ask for the best uniform contraction factor that holds across the whole budget. The theorem names the exact factor, one minus kappa over twice the budget's upper endpoint, proves it works everywhere on the budget, and proves nothing smaller can: the rate is attained at the budget's edge.
Generation one of the breeder's sustained pass. The parent contraction theorem said the budget factor is admissible; this theorem says it is the least admissible factor, an exact optimum rather than a bound. That exactness is the surface generation two stands on.
IsLeast {q : ℝ | ∀ r : ℝ, 1 / 2 ≤ r → Cost.Jcost r ≤ c → |phiCouplingNewRatio kappa r - 1| ≤ q * |r - 1|} (1 - kappa / (2 * Cost.jcostSublevelHi c))Claim boundaryTHEOREM for the formalized phantom-coupling model over the positive J-cost sublevel; sharpness is attained at the upper sublevel endpoint. One correction pass was used and disclosed. No world-first or priority claim.
-
CW-0013 · admitted 2026-07-19
Later radiation fits inside earlier capacity
Choose any two channel ticks with the first no later than the second. The radiation entropy at the later tick cannot exceed the channel capacity that remained at the earlier tick.
Adds a reusable cross-time Page-curve bound to the canonical Holography chapter. It is also the first public theorem minted by Cambrian after learning a new inequality-composition move from its own typed wall receipts.
∀ (ch : FiniteChannel) (t2 t1 : ℕ), t1 ≤ t2 → ch.radiationEntropy t2 ≤ ch.remainingCapacity t1Claim boundaryTHEOREM for the finite-channel PageCurve model: later radiation entropy is bounded by earlier remaining capacity whenever the ticks are ordered.
-
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, construct the topological carrier, or add semantics beyond the existing Wang inverse characterization. No world-first or priority claim (PRIORITY_UNRESOLVED).
-
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: exactly one integer parameter satisfies GoldenRelation. It does not derive the physical linking number from the kernel or construct the underlying topology. No world-first or priority claim (PRIORITY_UNRESOLVED).
-
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 world-first or priority claim (PRIORITY_UNRESOLVED).
-
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. The result carries no world-first or priority claim (PRIORITY_UNRESOLVED).
-
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 consequence is valid but only moderately independent, which lowered confidence to 0.82. No world-first or priority claim (PRIORITY_UNRESOLVED).
-
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 world-first or priority claim (PRIORITY_UNRESOLVED).
-
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 (PRIORITY_UNRESOLVED). This pair was a typed wall (MISSING_OPERATOR:translation-fiber-transport) for the previous operator set; 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 (PRIORITY_UNRESOLVED).
-
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 (PRIORITY_UNRESOLVED).
-
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 (PRIORITY_UNRESOLVED). 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 (PRIORITY_UNRESOLVED). The judge framed this as canonical lemma utility, smaller in scope than CW-0001; the same statement family had appeared as unlanded quarantine evidence inside the CW-0001 package and was re-authored end to end for this win.
-
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 (BP-4 spine). 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 (PRIORITY_UNRESOLVED). The counting scaffolding parent was hand-built; the winning statement and its held-out consequence were authored by the ordinary runner.