Masses Mass Genesis Anchor Amplitude Primitive Primitive Amplitude Cp6 Of Primit

The amplitude equivalence

In physics, a mass can often be written two ways: as a squared length, the norm of a state vector, or as an explicit product of factors that carry the physical meaning. The Recognition Science framework's machine-checked library of formal theorems proves that for its primitive mass patterns these two descriptions are interchangeable. The declaration primitiveAmplitudeCP6_of_primitiveAmplitudeNorm is the proof of one direction: if a pattern satisfies the norm condition, then it also satisfies the product condition. The reverse direction is proved separately, and together they form an exact equivalence.

The norm condition states that the squared size of a neutralized eight-component pattern equals the square of a single amplitude. The product condition states that the same neutralized pattern can be written as that amplitude times a unit chord, a vector of length one. The theorem shows these are the same requirement, not two independent constraints. This matters because the product form is the one that connects to the next stage of the framework's mass derivation, the CP6 target. The equivalence means a pattern that meets either condition is ready for that next step.

In Recognition Science, this is a step in a longer chain. The framework models mass as emerging from a discrete record of recognition events, and this declaration is one link in that chain. The proof itself is a formal theorem, checked by the machine, with no gaps and no extra axioms beyond the standard logical ones. It establishes a clean logical bridge between two formulations of the same physical condition.

What the declaration does not claim is just as important. It does not prove that any actual pattern satisfies either condition. It does not derive the chord from the framework's deeper dynamics. It does not produce a numerical mass value. The theorem is conditional: if a pattern meets the norm condition, then it meets the product condition. The existence of such a pattern, and the final mass value, remain open targets in the framework's program.

For a reader, the practical upshot is a guarantee of logical consistency. The framework can use whichever formulation is more convenient at a given stage, knowing the two cannot diverge. That is a modest but real result, and it keeps the larger mass-genesis project on a firm footing.

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

What this page does not claim

The theorem does not prove that any pattern satisfies either condition. The theorem does not derive the chord from Q3 or Rhat dynamics. The theorem does not produce a numerical mass value.

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: