Masses Mass Genesis Anchor Norm Primitive

The primitive anchor norm

In the Recognition Science framework, a particle's mass is not a free parameter but a quantity that must be consistent with a ledger, a discrete record of recognition events. The framework's library of machine-checked formal theorems has already assembled a long chain of implications, called the Mass Genesis chain, that leads from a fully expanded norm condition to statements about rest mass, inertial mass, and gravitational mass. The module described here, AnchorNormPrimitive, opens that fully expanded norm target into two physical pieces: a sector base load and a phi transport factor.

The sector base load is the sector yardstick divided over the eight occupied phases. The phi transport factor is selected by the topology-derived rung and charge skew. The module proves that this transport factor splits into two independent parts: a rung-only part and a charge-skew part. The charge-skew part, in turn, is proved to be exactly equal to a ratio of the form 1 plus Z over phi, where Z is a nonnegative integer label derived from the topology. All of these factors are proved to be positive.

The central theorem is an equivalence. The primitive factor norm, which states that the norm squared of the neutralized phase-zero window equals the sector base load times the phi transport factor, is proved to be equivalent to the fully expanded norm. This means that the simpler, factored form is definitionally sufficient for the entire Mass Genesis chain. The module packages this into a certificate, AnchorNormPrimitiveCert, which records the positivity proofs, the equivalence, and the fact that the primitive factor norm closes the full chain to rest mass and the equality of inertial and gravitational mass.

What this establishes in plain language is a cleaner target. Instead of working with the fully expanded norm, which is a complicated expression, one can work with the product of two factors: a base load set by the topology sector, and a phi transport factor set by rung and charge skew. The module proves that these two formulations are exactly the same condition, so any proof using the simpler form is valid for the full chain. This is a definitional and logical simplification, not a new physical derivation; the module explicitly does not prove either piece from dynamics.

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

theorem full_chain_for_primitiveFactorNorm
    (T : StableLoadReadoutTheory (Fin 8))
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hprimitive : AnchorPhasePrimitiveFactorNorm ψ) :
    (∀ k : ℕ,
      integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
    0 < restMass ψ ∧
    PhiRungQuantized ψ ∧
    restMass ψ = predictedMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ :=
  E.full_chain_for_fully_expanded_norm T
    (fullyExpandedNorm_of_primitiveFactorNorm ψ hprimitive)

What this page does not claim

This module does not prove either the sector base load or the phi transport factor from dynamics. This module does not derive the value of the golden ratio phi or any other constant; it uses them as given by the framework. This module does not compare predicted masses against measured PDG values.

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: