Masses Mass Genesis Anchor Norm Primitive Primitive Factor Norm Of Fully Expande

The primitive factor form

The declaration primitiveFactorNorm_of_fullyExpandedNorm is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a logical equivalence between two ways of writing a norm condition for a particle pattern. The first way, called the fully expanded norm, is a long expression that combines many terms. The second way, called the primitive factor norm, is a shorter product of two factors: a sector base load and a phi transport factor. The theorem states that if the fully expanded norm holds, then the primitive factor norm holds, and vice versa.

The sector base load is defined as a value divided by eight, where the numerator involves powers of 2 and the golden ratio phi. The phi transport factor is a power of phi, where the exponent depends on a rung number and a charge skew. The theorem itself is a rewriting result: it shows that the two expressions are interchangeable. It does not prove that either expression is the correct physical law for particle masses. The docstring for the module is explicit on this point: it states that the module does not prove either piece from dynamics.

The theorem also connects to a larger chain of results. If the primitive factor norm holds, then a full chain of consequences follows: the integrated meaning load is conserved under evolution, the rest mass is positive, the rest mass equals the predicted mass, and the inertial and gravitational masses both equal the rest mass. These consequences are proved in the library, but they all depend on the primitive factor norm being assumed. The theorem does not show that any actual particle satisfies this norm.

In plain terms, the declaration is a bridge between two notations. It lets the framework's library switch from a long expanded formula to a compact product form when convenient. It also provides a certificate that the product form is positive and that the two forms are equivalent. But the physical content, whether the norm actually holds for real particles, is not part of this theorem. That remains a separate question, open to empirical check against measured masses.

theorem primitiveFactorNorm_of_fullyExpandedNorm
    (ψ : LightPattern (Fin 8))
    (hfull : AnchorPhaseFullyExpandedNorm ψ) :
    AnchorPhasePrimitiveFactorNorm ψ :=
  (primitiveFactorNorm_iff_fullyExpandedNorm ψ).2 hfull

theorem primitiveFactorNorm_of_fullyExpandedNorm
    (ψ : LightPattern (Fin 8))
    (hfull : AnchorPhaseFullyExpandedNorm ψ) :
    AnchorPhasePrimitiveFactorNorm ψ :=
  (primitiveFactorNorm_iff_fullyExpandedNorm ψ).2 hfull

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 theorem does not prove that any actual particle satisfies the primitive factor norm. The theorem does not derive the primitive factor norm from the dynamics of recognition events. The theorem does not compare the predicted masses against measured particle masses.

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: