Masses Mass Genesis T10 Anchor Load Transport Composition Phi Component Ne Zero

The irrationality condition

In the Recognition Science framework, particle masses are not free parameters. A chain of theorems forces a specific formula, and this declaration is a key step in showing that formula has a surprising consequence: the predicted mass of a charged particle is never a simple fraction. The result is a theorem in the framework's machine-checked library of formal theorems, meaning it is proved from axioms and cannot be false within the framework's logic.

The mass formula itself looks complicated, but its structure is what matters. The framework predicts a mass for a particle based on its sector and rung, and the formula can be rewritten as a power of 2 times an expression involving the golden ratio φ. That expression has two parts: a rational part and an irrational part, the part multiplied by φ. The declaration phi_component_ne_zero_of_transport_pos proves that this irrational part is never zero, provided the transport count is at least one and the charge skew Z is non-negative. A nonzero irrational part means the whole mass is irrational, and therefore cannot be a ratio of two integers.

This matters because of what it rules out. The framework's ledger of recognition events must produce a specific load to match the predicted mass. If that load could be a rational number, then many simple mechanisms could produce it: stacking postings coherently, stacking them incoherently, or any combination of the eight settlement postings with rational weights. The theorem shows all of these fail. The required load is irrational, so no rational composition of postings can ever match it. This is a field obstruction, not a numerical accident.

In Recognition Science, this is the point where the framework proves a negative result. It does not prove what the correct mechanism is. The theorem only shows that the mechanism must introduce irrationality of its own, specifically a power of φ. The framework introduces a candidate operation, rungTransport, which multiplies a posting by √φ and scales the load by φ, but this operation is introduced as a definition, not derived. Whether the ledger actually has such an operation remains an open question. The theorem establishes the shape any successful mechanism must have, not the mechanism itself.

The theorem also does not claim that the transport count is a physical number of operations. The framework reads the count from the topology, but it does not derive that reading from first principles. That interpretation is assumed, not proved. The declaration is a precise algebraic statement about the mass formula, and its power is in what it excludes: a whole family of rational explanations for the anchor load.

/-- The `φ`-component hypothesis discharged from the transport count. -/
theorem phi_component_ne_zero_of_transport_pos
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z)
    (hn : 1 ≤ Anchor.r0 s + r - 14) :
    Int.fib (Anchor.r0 s + r - 13)
        + Z * Int.fib (Anchor.r0 s + r - 14) ≠ 0 := by
  have hpos := phi_component_pos hn hZ
  have hidx : Anchor.r0 s + r - 14 + 1 = Anchor.r0 s + r - 13 := by ring
  rw [hidx] at hpos
  exact ne_of_gt hpos

/-- **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

/-- **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)

/-- One rung of transport. -/
def rungTransport (w : PhotonWindow) : PhotonWindow :=
  fun t => (Real.sqrt Constants.phi : ℂ) * w t

What this page does not claim

The theorem does not prove that the ledger has a rungTransport operation. The theorem does not derive the transport count from first principles; it reads it from supplied topology. The theorem does not identify the physical mechanism that produces the irrational load.

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: