Masses Mass Genesis Anchor Norm Primitive Canonical Primitive Load Factorizes Of

The factorization bridge

The declaration canonicalPrimitiveLoadFactorizes_of_primitiveFactorNorm is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states a conditional bridge: if a physical pattern ψ satisfies a certain norm law, and if there is evidence that the pattern is Q3-closed (meaning its topology is consistent with the framework's eight-phase structure), then the pattern's canonical primitive load factorizes. Factorization here means the load splits cleanly into two independent pieces: a sector base load, which is the topology's yardstick divided over eight phases, and a phi transport factor, which depends on the pattern's rung and charge skew.

What makes the theorem useful is the equivalence it rests on. The framework proves that the primitive factor norm, the simple two-factor formula, is logically equivalent to the fully expanded anchor norm, a much more detailed expression. This equivalence is a theorem, not an assumption. The declaration then uses that equivalence to close the gap: given the simple factor norm and the Q3-closed evidence, the full expanded norm follows, and with it the factorization. The chain from the simple formula to the full mass properties is definitionally sufficient, meaning the framework's existing machinery applies directly without further work.

The theorem does not prove that any physical pattern actually satisfies the primitive factor norm. That is a separate claim, an open target. The declaration only says: if the norm holds and the evidence is present, then factorization follows. It also does not derive the values of the sector base load or the phi transport factor from dynamics; those are definitional choices in the framework, not results. The positivity of the factors is proved, as is the equivalence between the primitive and expanded norms, but the physical origin of the norm itself remains unproved.

For a reader, the practical consequence is a simplification. The framework's mass chain can be checked at a simpler landing surface, the two-factor primitive norm, instead of the fully expanded one. The theorem guarantees that no information is lost in the simplification. What it does not guarantee is that the simpler surface is actually occupied by any real pattern in the framework. That is the next question the framework leaves open, and it is the one that would turn this structural bridge into a physical prediction.

theorem canonicalPrimitiveLoadFactorizes_of_primitiveFactorNorm
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hprimitive : AnchorPhasePrimitiveFactorNorm ψ) :
    CanonicalPrimitiveLoadFactorizes ψ :=
  E.canonicalPrimitiveLoadFactorizes_of_fully_expanded_norm
    (fullyExpandedNorm_of_primitiveFactorNorm ψ 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 primitiveAnchorSectorLoad_pos (ψ : LightPattern (Fin 8)) :
    0 < primitiveAnchorSectorLoad ψ := by
  unfold primitiveAnchorSectorLoad Anchor.E_coh
  exact div_pos
    (mul_pos
      (mul_pos
        (zpow_pos (by norm_num : (0 : ℝ) < 2) _)
        (zpow_pos Constants.phi_pos _))
      (zpow_pos Constants.phi_pos _))
    (by norm_num)

theorem primitivePhiTransport_pos (ψ : LightPattern (Fin 8)) :
    0 < primitivePhiTransport ψ := by
  unfold primitivePhiTransport
  exact Real.rpow_pos_of_pos Constants.phi_pos _

What this page does not claim

The theorem does not prove that any pattern satisfies the primitive factor norm. The theorem does not derive the factor values from dynamics. The theorem does not establish the physical origin of the norm itself.

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: