Masses Mass Genesis Anchor Norm Primitive Primitive Phi Transport Eq Rung Mul Ch

The transport split

The golden ratio φ, about 1.618, is the number that solves r² = r + 1. In the Recognition Science framework, particle masses are built on a ladder of powers of φ, and the declaration primitivePhiTransport_eq_rung_mul_charge is a proved identity about how one rung of that ladder factors. It states that the full φ-transport factor for a pattern, which is φ raised to a power that mixes a rung index and a charge label, equals the product of two separate φ-powers: one depending only on the rung, and one depending only on the charge. The proof is a single algebraic step: φ^(a+b) = φ^a · φ^b, applied after rewriting the charge part as a logarithm.

The rung part is φ^((rung − 8)), so a pattern eight rungs up gets no rung transport at all. The charge part is φ^(log(1 + Z/φ) / log φ), which by the definition of a logarithm is just the number 1 + Z/φ itself. So the theorem is not only a formal split; it also rewrites the charge transport as a simple ratio. The full transport factor is therefore φ^(rung − 8) · (1 + Z/φ). The declaration is a theorem, a statement proved in the framework's machine-checked library of formal theorems, and it is axiom-clean: it relies only on the standard properties of real powers and logarithms.

What the theorem does not do is just as important as what it does. It does not derive the rung or charge factors from any physical law; the framework's own documentation says it states the next exact landing surface and does not prove either piece from dynamics. The rung index and charge label come from a pattern's topology, but the theorem only says that if those labels are given, the transport factor splits as claimed. It also does not establish that any particle's mass equals the predicted value. That equality is a separate target, bundled in a larger chain that requires additional evidence about closed patterns and stable readouts. The split is a structural fact about how the mass formula is organized, not a proof that the formula matches measurement.

The practical consequence is that the mass-genesis calculation can be assembled from two independent pieces: a sector base load, which carries the topology's main weight, and the φ-transport factor, which now separates into a rung contribution and a charge contribution. This factorization is what lets the framework's mass chain be expressed in a primitive, factored form that is definitionally equivalent to the fully expanded norm. A reader can now see the mass formula as a product of three named ingredients: the sector load, the rung power, and the charge ratio, each with a clear meaning, and each a candidate for separate future derivation.

/-- The phi transport factor splits into independent rung and charge-skew
transport factors. -/
theorem primitivePhiTransport_eq_rung_mul_charge
    (ψ : LightPattern (Fin 8)) :
    primitivePhiTransport ψ =
      primitiveRungTransport ψ * primitiveChargeSkewTransport ψ := by
  unfold primitivePhiTransport
  unfold primitiveRungTransport
  unfold primitiveChargeSkewTransport
  rw [Real.rpow_add Constants.phi_pos]

theorem primitiveChargeSkewTransport_eq_ratio
    (ψ : LightPattern (Fin 8)) :
    primitiveChargeSkewTransport ψ = primitiveChargeSkewRatio ψ := by
  unfold primitiveChargeSkewTransport
  unfold primitiveChargeSkewRatio
  change Constants.phi ^
      (Real.logb Constants.phi (1 + (ZOf ψ : ℝ) / Constants.phi)) =
    1 + (ZOf ψ : ℝ) / Constants.phi
  exact Real.rpow_logb Constants.phi_pos Constants.phi_ne_one
    (by simpa [primitiveChargeSkewRatio] using primitiveChargeSkewRatio_pos ψ)

theorem primitiveFactorNorm_iff_fullyExpandedNorm
    (ψ : LightPattern (Fin 8)) :
    AnchorPhasePrimitiveFactorNorm ψ ↔ AnchorPhaseFullyExpandedNorm ψ := by
  unfold AnchorPhasePrimitiveFactorNorm AnchorPhaseFullyExpandedNorm
  unfold primitiveAnchorSectorLoad primitivePhiTransport
  have hright :
      (((2 : ℝ) ^ Anchor.B_pow (sectorOf ψ) *
          Anchor.E_coh *
          Constants.phi ^ Anchor.r0 (sectorOf ψ)) *
          Constants.phi ^
            (((rungOf ψ : ℝ) - 8) +
              Real.log (1 + (ZOf ψ : ℝ) / Constants.phi) /
                Real.log Constants.phi)) /
          (8 : ℝ) =
        ((2 : ℝ) ^ Anchor.B_pow (sectorOf ψ) *
          Anchor.E_coh *
          Constants.phi ^ Anchor.r0 (sectorOf ψ)) /
          (8 : ℝ) *
        Constants.phi ^
          (((rungOf ψ : ℝ) - 8) +
            Real.log (1 + (ZOf ψ : ℝ) / Constants.phi) /
              Real.log Constants.phi) := by
    ring
  constructor
  · intro h
    rw [hright]
    exact h
  · intro h
    rw [← hright]
    exact h

What this page does not claim

The theorem does not prove either the rung or the charge transport factor from dynamics. The theorem does not establish that any particle's rest mass equals the framework's predicted mass. The theorem does not show that the golden ratio itself is the unique scaling for masses; that is a separate result.

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/AnchorNormPrimitive.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: