Encyclopedia Masses Masses Mass Genesis T10 Anchor Load Transport Composition Charged Row Required L

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Anchor Load Transport Composition Charged Row Required L

A machine-checked proof shows that no rational combination of postings can carry the load that charged particles demand, leaving a precise gap for future physics.

Verify this page

Why stacking fails

In the Recognition Science account, a ledger is a discrete record of events, and each event is a posting, a unit entry in that record. The framework assigns each particle a required load, a number that its posting window must reach. The declaration chargedRow_required_load_ne_compositePosting proves a negative result: for every charged fermion row in the framework's mass table, the required load can never equal the load of any composite posting built from rational multiples of the eight settlement postings. A composite posting is a superposition, a weighted sum of the eight basic postings, with weights chosen from the rational numbers. The proof shows that any such composite has a rational load, while the required load for a charged row is irrational, so the two cannot match.

The result is a field obstruction, not a numerical accident. The framework's mass law, with its logarithm removed, gives the predicted mass as a dyadic rational times an element of the ring Z[φ], where φ is the golden ratio. The φ-component is nonzero for every charged row, making the mass irrational, and therefore the required load, the mass divided by eight, is also irrational. Any composite posting with rational weights has a load that is rational, because the eight settlement postings have rational coordinates and the neutralization operation preserves that rationality. The theorem required_load_ne_compositePosting states this for a general sector, and chargedRow_required_load_ne_compositePosting applies it to the nine charged rows. This excludes not only the simple cases of coherent stacking, where N identical postings add in phase to give a load of 2N², and incoherent stacking, where they are orthogonal and give 2N, but also every superposition between them, including interference cross terms.

The proof is a theorem in the framework's machine-checked library of formal theorems, with no unproved assumptions. The key hypothesis, that the φ-component is nonzero, is discharged for the charged rows by a separate lemma, not assumed. The down-type sector's light rungs, which have a negative transport count, are covered by a numerical receipt rather than the general lemma, but the exclusion for them is still established.

What the declaration does not claim is as important as what it proves. It does not exhibit any mechanism that does carry the required load. It only shows that a whole family of rational-composition mechanisms cannot. The framework introduces a candidate operation, called rungTransport, which multiplies a posting by the square root of φ and scales its load by φ, and it proves that the required load equals the load of such a transported posting times sector and charge factors. But the docstring is explicit: rungTransport is introduced here, nothing proves the ledger has such an operation, and the choice of √φ was made precisely so the load would scale by φ. Whether the ledger actually supplies this transport is an open question, not a theorem.

The practical consequence is a sharpened target. The framework now knows the shape any successful mass-generation mechanism must have: a per-rung multiplicative factor of φ, with the count in the exponent. The transport count itself is read off the topology, not derived, and the interpretation of that count as a number of physical operations is an assumption. The declaration narrows the search space and names the missing piece, but it does not fill the gap.

THEOREM chargedRow_required_load_ne_compositePosting · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
chargedRow_required_load_ne_compositePosting · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:475 
/-- **No charged fermion's required anchor load is reachable by any rational
composition of postings.** All nine rows, by theorem rather than by receipt. -/
theorem chargedRow_required_load_ne_compositePosting
    (row : ChargedMassRow) (n : Fin 8 → ℚ) :
    MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) / 8
      ≠ normSq8 (neutralize (compositePosting n)) := by
  refine required_load_ne_compositePosting _ _ _ ?_ (phi_component_ne_zero_of_chargedRow row) n
  cases row <;> simp [rowZ]
THEOREM compositePosting_gaussianRational · gaussianRational_load_rat · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
compositePosting_gaussianRational · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:405 
theorem compositePosting_gaussianRational (n : Fin 8 → ℚ) :
    GaussianRationalWindow (compositePosting n) :=
  gaussianRational_ratCombination n commitSettlementWindow
    commitSettlementWindow_gaussianRational
gaussianRational_load_rat · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:348 
/-- **Rational ticks give a rational load.** Both terms of the neutralization
identity are then rational, so no cross term can escape into the irrationals. -/
theorem gaussianRational_load_rat {w : PhotonWindow} (hw : GaussianRationalWindow w) :
    ∃ c : ℚ, normSq8 (neutralize w) = (c : ℝ) := by
  choose a b hab using hw
  refine ⟨(∑ i : Fin 8, (a i ^ 2 + b i ^ 2))
      - ((∑ i : Fin 8, a i) ^ 2 + (∑ i : Fin 8, b i) ^ 2) / 8, ?_⟩
  rw [normSq8_neutralize_eq]
  have h1 : normSq8 w = ∑ i : Fin 8, (((a i : ℝ)) ^ 2 + ((b i : ℝ)) ^ 2) := by
    simp only [normSq8, Complex.normSq_apply]
    exact Finset.sum_congr rfl (fun i _ => by rw [(hab i).1, (hab i).2]; ring)
  have hre : (∑ j : Fin 8, w j).re = ∑ j : Fin 8, ((a j : ℝ)) := by
    rw [Complex.re_sum]
    exact Finset.sum_congr rfl (fun j _ => (hab j).1)
  have him : (∑ j : Fin 8, w j).im = ∑ j : Fin 8, ((b j : ℝ)) := by
    rw [Complex.im_sum]
    exact Finset.sum_congr rfl (fun j _ => (hab j).2)
  rw [h1, Complex.normSq_apply, hre, him]
  push_cast
  ring
THEOREM required_load_ne_compositePosting · required_load_irrational · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
required_load_ne_compositePosting · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:421 
/-- **The whole additive family, excluded in one statement.** No composite posting,
at any rational multiplicities across the eight phases and with every interference
cross term included, carries the anchor load the normalization condition requires.
The two named counting laws are the aligned and orthogonal extremes of this family. -/
theorem required_load_ne_compositePosting
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hp : Int.fib (Anchor.r0 s + r - 13)
            + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0) (n : Fin 8 → ℚ) :
    MassLaw.predict_mass s r Z / 8 ≠ normSq8 (neutralize (compositePosting n)) :=
  required_load_ne_gaussianRational_load s r Z hZ hp
    (compositePosting_gaussianRational n)
required_load_irrational · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:233 
/-- The required anchor load is irrational. -/
theorem required_load_irrational
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hp : Int.fib (Anchor.r0 s + r - 13)
            + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0) :
    Irrational (MassLaw.predict_mass s r Z / 8) :=
  (predict_mass_irrational s r Z hZ hp).div_intCast (by norm_num : (8 : ℤ) ≠ 0)
THEOREM required_load_ne_coherent_count · required_load_ne_incoherent_count · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
required_load_ne_coherent_count · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:264 
/-- **Coherent composition fails.** `N` aligned unit postings carry load `2 N²`,
which `alignedPostings_load` below derives rather than assumes. -/
theorem required_load_ne_coherent_count
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hp : Int.fib (Anchor.r0 s + r - 13)
            + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0) (N : ℕ) :
    MassLaw.predict_mass s r Z / 8 ≠ 2 * (N : ℝ) ^ 2 := by
  have h := required_load_ne_rat s r Z hZ hp (2 * (N : ℚ) ^ 2)
  intro heq
  exact h (by rw [heq]; push_cast; ring)
required_load_ne_incoherent_count · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:253 
/-- **Incoherent composition fails.** `N` unit postings whose neutralizations are
mutually orthogonal carry load `2 N`, since the cross terms vanish. -/
theorem required_load_ne_incoherent_count
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hp : Int.fib (Anchor.r0 s + r - 13)
            + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0) (N : ℕ) :
    MassLaw.predict_mass s r Z / 8 ≠ 2 * (N : ℝ) := by
  have h := required_load_ne_rat s r Z hZ hp (2 * N)
  intro heq
  exact h (by rw [heq]; push_cast; ring)
THEOREM rungTransport_load · required_load_eq_transportedLoad_mul · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
rungTransport_load · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:520 
/-- Transport multiplies the neutralized load by `φ`. -/
theorem rungTransport_load (w : PhotonWindow) :
    normSq8 (neutralize (rungTransport w))
      = Constants.phi * normSq8 (neutralize w) := by
  have hsq : Real.sqrt Constants.phi ^ 2 = Constants.phi :=
    Real.sq_sqrt Constants.phi_pos.le
  have hshape : rungTransport w
      = fun t => ((Real.sqrt Constants.phi : ℝ) : ℂ) * w t := rfl
  rw [hshape, normSq8_neutralize_smul, hsq]
required_load_eq_transportedLoad_mul · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:552 
/-- **Closed-form rearrangement.** The anchor load
`LoadNormalizedToTopology` demands equals the modeled load of one unit posting
after `r0 + rung - 14` scalar iterations, times the sector's cube-geometry
factor `2 ^ (B - 4)` and charge skew `φ + Z`. The factors are the mass law's own
data, but this equality does not derive a ledger composition or physical rung
transition. -/
theorem required_load_eq_transportedLoad_mul
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z) :
    MassLaw.predict_mass s r Z / 8
      = transportedLoad (Anchor.r0 s + r - 14) *
          ((2 : ℝ) ^ (Anchor.B_pow s - 4) * (Constants.phi + (Z : ℝ))) := by
  have hsplit : (2 : ℝ) ^ (Anchor.B_pow s - 4)
      = (2 : ℝ) ^ (Anchor.B_pow s) / 16 := by
    rw [show (Anchor.B_pow s - 4) = Anchor.B_pow s + (-4 : ℤ) by ring,
      zpow_add₀ (by norm_num : (2 : ℝ) ≠ 0),
      show ((2 : ℝ) ^ (-4 : ℤ)) = 1 / 16 by norm_num]
    ring
  rw [predict_mass_eq_phi_zpow_mul s r Z hZ, transportedLoad, hsplit]
  ring

What this page does not claim

This does not prove that any mechanism can carry the required load, only that rational compositions cannot. This does not claim that the rungTransport operation exists in the ledger; it is introduced as a candidate. This does not derive the transport count from the topology; it is read off as an input.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND