Masses Mass Genesis T10 Anchor Load Transport Composition Required Load Eq Trans

The transport target

The Recognition Science framework models particle masses as a required load: a number that a pattern of eight settlement postings must reach. The declaration required_load_eq_transported_unitPosting establishes an algebraic identity. It says that for any sector, rung, and charge skew, the required load equals the load of a single unit posting that has been transported k times, multiplied by a sector factor and a charge skew. The transport count k is read off the topology, and the unit posting is a specific eight-tick window.

The identity is a rearrangement of a closed form for the mass law, not an independent discovery. The mass law's exponent, which looks transcendental, collapses against its base: φ^gap(Z) = 1 + Z/φ. Folding this collapse into the yardstick gives predictedMass = 2^B · φ^(r0 + rung - 14) · (φ + Z), with every exponent an integer. The theorem required_load_eq_transported_unitPosting then unfolds the transported load, which is defined as 2 · φ^k, and rearranges the closed form to match. The scalar √φ was chosen precisely so that the load scales by φ per rung, so the transport algebra is a property of that choice, not evidence for it.

What the theorem does not claim is that the ledger actually has such a transport operation. The operation rungTransport, which multiplies a window by √φ, is introduced here; nothing proves the ledger supplies it, and no theorem exhibits a physical window undergoing it. The transport count is read off the topology, not derived: the mass law accepts rung as an input, and reading r0 + rung - 14 as a number of physical operations is an interpretation the module assumes. Whether the ledger supplies the transport law is open.

The theorem's value is as a target. It states the shape any successful mechanism must have: a per-rung multiplicative factor of φ with the count in the exponent. This sharpens the successor residual from asking for a multiplicity law to asking for a transport law. The exclusion that precedes it, that no rational composition of postings carries the anchor load, is a field obstruction rather than an unlucky set of numbers. The transport target is the algebraic form that survives it.

/-- The same statement with the transport written as an explicit iteration, for the
sectors whose transport count is nonnegative. -/
theorem required_load_eq_transported_unitPosting
    (s : Anchor.Sector) (r Z : ℤ) (hZ : 0 ≤ Z) (k : ℕ)
    (hk : (k : ℤ) = Anchor.r0 s + r - 14) :
    MassLaw.predict_mass s r Z / 8
      = normSq8 (neutralize (rungTransport^[k] unitPosting)) *
          ((2 : ℝ) ^ (Anchor.B_pow s - 4) * (Constants.phi + (Z : ℝ))) := by
  rw [required_load_eq_transportedLoad_mul s r Z hZ, ← hk, transportedLoad_natCast]

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

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

/-- 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 transport operation. The theorem does not derive the transport count from the topology. The theorem does not establish that the transport algebra is physically realized.

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: