Encyclopedia Masses Masses Mass Genesis T10 Anchor Load Transport Composition

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Anchor Load Transport Composition

A machine-checked proof shows that no rational combination of postings can carry the anchor load required for charged fermion masses, leaving a specific algebraic target for a future transport law.

Verify this page

The load ceiling

In the Recognition Science framework, particle masses are not free parameters. The framework's library of formal theorems derives a mass law from a small set of axioms, and that law assigns a predicted mass to each charged fermion. The mass law's formula contains a term that looks transcendental, but a theorem in the library shows that the logarithm in the exponent collapses against its base, leaving a closed form with only integer exponents and an integer charge term. This collapse is the key that lets the framework ask a sharp question: can the required mass be produced by a simple composition of more basic objects?

The answer, proved in the module T10AnchorLoadTransportComposition, is no. The framework models a charged fermion's mass as requiring a certain anchor load, a number derived from the mass law divided by eight. The module proves that this required load is irrational for all charged fermion rows except three light down-type quarks, which are covered by a numerical check. Because the load is irrational, it cannot equal the load of any window formed by a rational superposition of the eight settlement postings, which always has a rational load. This excludes coherent stacking, where loads add as squares, incoherent stacking, where they add linearly, and the entire family of rational superpositions between them. The obstruction is structural, not a numerical accident.

What survives the exclusion is a precise target. The closed form shows that the missing irrationality is a power of the golden ratio φ. The module introduces a hypothetical operation called rung transport that multiplies a posting's amplitude by the square root of φ. Iterating this operation k times on a single unit posting produces a load of 2φ^k, which matches the required load up to a known sector factor and charge skew. The module proves this equality, but it is careful to admit that rung transport is introduced here, not derived from the ledger's axioms, and that the scalar √φ was chosen precisely to make the load scale by φ. The transport law itself remains an open question.

The module also notes that the transport count is read off the topology, not derived from it, and that the interpretation of that count as a number of physical operations is an assumption. The result sharpens the problem: instead of asking how many postings compose into an anchor, the framework now asks what law of transport could supply the required per-rung factor of φ. This is a more constrained question, and the module provides the algebraic shape any successful answer must take.

THEOREM predict_mass_irrational · required_load_irrational · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
predict_mass_irrational · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:209 
/-- **The predicted mass is irrational** whenever its `φ`-component is nonzero.
The `φ`-component is `F (r0 + rung - 13) + Z · F (r0 + rung - 14)`. -/
theorem predict_mass_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) := by
  set p : ℤ := Int.fib (Anchor.r0 s + r - 13)
      + Z * Int.fib (Anchor.r0 s + r - 14) with hpdef
  set q : ℤ := Int.fib (Anchor.r0 s + r - 14)
      + Z * Int.fib (Anchor.r0 s + r - 15) with hqdef
  have hpair : Irrational ((p : ℝ) * Constants.phi + (q : ℝ)) :=
    (Constants.PhiLadder.phi_irrational.intCast_mul hp).add_intCast q
  have htwo : ((2 : ℚ) ^ (Anchor.B_pow s) : ℚ) ≠ 0 :=
    zpow_ne_zero _ (by norm_num)
  have hcast : (((2 : ℚ) ^ (Anchor.B_pow s) : ℚ) : ℝ)
      = (2 : ℝ) ^ (Anchor.B_pow s) := by
    push_cast
    ring
  have := hpair.ratCast_mul htwo
  rw [hcast] at this
  rw [predict_mass_eq_fib_pair s r Z hZ]
  exact this
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_compositePosting · gaussianRational_load_rat · 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)
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 transportedPosting_load · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
transportedPosting_load · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean:530 
/-- **`k` iterations of the modeled scalar map on one unit posting carry load
`2 φ^k`.** This is an algebraic iteration of `rungTransport`, not a derived
composition of ledger postings or a topology transition. -/
theorem transportedPosting_load (k : ℕ) :
    normSq8 (neutralize (rungTransport^[k] unitPosting))
      = 2 * Constants.phi ^ k := by
  induction k with
  | zero => simpa using unitPosting_load
  | succ n ih =>
      rw [Function.iterate_succ_apply', rungTransport_load, ih]
      ring
THEOREM required_load_eq_transportedLoad_mul · IndisputableMonolith/Masses/MassGenesis/T10AnchorLoadTransportComposition.lean
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

The module does not derive a transport law; it only states the algebraic shape such a law must have. The module does not prove that rung transport exists in the framework's ledger. The module does not derive the transport count from the topology; it reads it 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