Masses Mass Genesis Anchor Norm Primitive Fully Expanded Norm Of Primitive Facto

The primitive factor route

In the Recognition Science framework, particle masses are meant to emerge from a discrete record of recognition events. The framework's library, a machine-checked collection of formal theorems, contains a theorem named fullyExpandedNorm_of_primitiveFactorNorm. It states that if a certain simplified norm condition holds for a light pattern, then the full expanded norm condition also holds. The simplified condition, called the primitive factor norm, expresses the squared norm of a neutralized phase as a product of two factors: a sector base load and a phi transport factor. The full expanded norm is the more detailed target that the mass-genesis chain requires.

The theorem is a bridge, not a discovery. It proves an equivalence: the primitive factor norm holds if and only if the fully expanded norm holds. This means the two conditions are definitionally interchangeable. The proof is a direct application of the equivalence theorem primitiveFactorNorm_iff_fullyExpandedNorm. The declaration does not prove that either norm actually holds for any physical pattern. It only shows that if one holds, the other does too. The primitive factor norm itself is a definitional choice, a way of splitting the full target into two pieces: the sector base load, which is the sector yardstick divided over eight occupied phases, and the phi transport factor, which depends on the rung and charge skew.

The theorem's real work is downstream. Given the primitive factor norm and additional evidence, the library proves a full chain of consequences: the integrated meaning load is invariant under evolution, the rest mass is positive, the phi rung is quantized, the rest mass equals the predicted mass, and the inertial and gravitational masses equal the rest mass. These consequences are theorems, but they all depend on the primitive factor norm being supplied as a hypothesis. The primitive factor norm is the entry ticket; the theorem opens the door to the rest of the mass-genesis chain.

What the declaration does not claim is equally important. It does not prove that the primitive factor norm follows from dynamics. The docstring is explicit: it does not prove either piece from dynamics. The sector base load and phi transport factor are selected by topology, rung, and charge skew, but their values are not derived from first principles. The theorem also does not claim that the primitive factor norm is physically realized. It is a conditional statement: if the norm holds, then the chain follows. Whether it holds for any actual pattern is a separate question, left open.

In practice, this theorem is a proof-engineering convenience. It lets the framework's library work with a simpler, factored form of the norm while knowing that the full target is equivalent. It is a step in a larger formalization, not a physical law. The distinction matters: the equivalence is proved, but the physical content of the norm is assumed. A reader should see the theorem as a reliable bridge over a gap that is already known to be bridgeable, not as evidence that the gap itself is closed.

theorem fullyExpandedNorm_of_primitiveFactorNorm
    (ψ : LightPattern (Fin 8))
    (hprimitive : AnchorPhasePrimitiveFactorNorm ψ) :
    AnchorPhaseFullyExpandedNorm ψ :=
  (primitiveFactorNorm_iff_fullyExpandedNorm ψ).1 hprimitive

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

The primitive factor norm is not derived from dynamics. The theorem does not establish that the primitive factor norm holds for any actual physical pattern. The theorem does not prove that the sector base load or phi transport factor values are physically necessary.

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: