Masses Mass Genesis Anchor Amplitude Primitive Primitive Amplitude Norm Of Primi

The amplitude norm bridge

In the Recognition Science framework, a particle's state is a pattern of eight complex numbers, a light pattern (a discrete record of recognition events). The framework's mass-genesis module studies two ways to characterize such a pattern. One is a geometric statement: the pattern, after a process called neutralization, can be written as a single amplitude times a unit chord, a vector of length one. The other is a numerical statement: the squared length of the neutralized pattern equals the square of that same amplitude. The theorem primitiveAmplitudeNorm_of_primitiveAmplitudeCP6 proves that the geometric statement implies the numerical one.

The proof is short and relies on two classical facts about complex numbers. First, scaling every component of a vector by a real number a multiplies its squared norm by a². Second, a unit chord has squared norm one. The theorem applies these to show that if the neutralized pattern equals the amplitude times a unit chord, then its squared norm is exactly the amplitude squared. This is the bridge: the geometric description forces the numerical norm to match, with no further assumptions.

The declaration does not claim the reverse direction, that the numerical norm forces the geometric description. That converse is a separate theorem, primitiveAmplitudeCP6_of_primitiveAmplitudeNorm, which the library also proves. Together they form an equivalence, primitiveAmplitudeCP6_iff_primitiveAmplitudeNorm, so the two characterizations are interchangeable for any pattern that satisfies either one. The bridge is two-way, but the theorem named in the question only establishes the one direction from geometry to norm.

Most importantly, the theorem does not claim that any actual particle satisfies the geometric statement. It is a conditional result: if a pattern has the geometric property, then it has the numerical one. Whether such patterns exist in the framework's dynamics is a separate question, addressed by other declarations that require additional evidence, such as a closed-pattern condition. The theorem itself is a logical implication, not an existence proof.

In Recognition Science, this implication is a step toward deriving particle masses from the framework's axioms. The full chain, full_chain_for_primitiveAmplitudeCP6, shows that if a pattern has the geometric property and satisfies a closed-pattern condition, then its rest mass is positive, quantized on the phi rung, and equals the predicted mass, with inertial and gravitational masses equal to it. The theorem in question is the first link in that chain, establishing the norm that the later results rely on.

theorem primitiveAmplitudeNorm_of_primitiveAmplitudeCP6
    (ψ : LightPattern (Fin 8))
    (hcp6 : AnchorPhasePrimitiveAmplitudeCP6 ψ) :
    AnchorPhasePrimitiveAmplitudeNorm ψ := by
  rcases hcp6 with ⟨u, hu⟩
  unfold AnchorPhasePrimitiveAmplitudeNorm
  rw [hu, normSq8_real_smul_fin8, u.normalized, mul_one]

theorem primitiveAmplitudeCP6_of_primitiveAmplitudeNorm
    (ψ : LightPattern (Fin 8))
    (hamp : AnchorPhasePrimitiveAmplitudeNorm ψ) :
    AnchorPhasePrimitiveAmplitudeCP6 ψ := by
  let a : ℝ := primitiveClosedPatternAmplitude ψ
  let v : Fin 8 → ℂ := neutralize (ψ.window 0)
  have ha_pos : 0 < a := by
    simpa [a] using primitiveClosedPatternAmplitude_pos ψ
  have ha_ne : a ≠ 0 := ne_of_gt ha_pos
  have hvnorm : normSq8 v = a ^ 2 := by
    simpa [AnchorPhasePrimitiveAmplitudeNorm, v, a] using hamp
  let u : IndisputableMonolith.LightLanguage.Geometry.NeutralMeaningManifold.NeutralUnitChord :=
    { chord := fun t => v t / (a : ℂ)
      neutral := neutral_real_div_fin8 a (neutralize_is_neutral (ψ.window 0))
      normalized := by
        calc
          normSq8 (fun t => v t / (a : ℂ))
              = normSq8 v / a ^ 2 := normSq8_real_div_fin8 a v
          _ = a ^ 2 / a ^ 2 := by rw [hvnorm]
          _ = 1 := by field_simp [pow_ne_zero 2 ha_ne] }
  refine ⟨u, ?_⟩
  ext t
  simp [u, v]
  exact (mul_div_cancel₀ (v t) (by exact_mod_cast ha_ne)).symm

theorem primitiveAmplitudeCP6_iff_primitiveAmplitudeNorm
    (ψ : LightPattern (Fin 8)) :
    AnchorPhasePrimitiveAmplitudeCP6 ψ ↔
      AnchorPhasePrimitiveAmplitudeNorm ψ := by
  constructor
  · exact primitiveAmplitudeNorm_of_primitiveAmplitudeCP6 ψ
  · exact primitiveAmplitudeCP6_of_primitiveAmplitudeNorm ψ

theorem primitiveAmplitudeNorm_of_primitiveAmplitudeCP6
    (ψ : LightPattern (Fin 8))
    (hcp6 : AnchorPhasePrimitiveAmplitudeCP6 ψ) :
    AnchorPhasePrimitiveAmplitudeNorm ψ := by
  rcases hcp6 with ⟨u, hu⟩
  unfold AnchorPhasePrimitiveAmplitudeNorm
  rw [hu, normSq8_real_smul_fin8, u.normalized, mul_one]

What this page does not claim

The theorem does not prove that any particle state actually has the geometric CP6 property. The theorem does not derive the unit chord from the framework's deeper Q3/Rhat dynamics. The theorem does not by itself establish any property of rest mass, quantization, or mass prediction; those require additional closed-pattern evidence.

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