Encyclopedia Masses Masses Mass Genesis Master Certificate Stable Closed Mass Genesis Chain From Pay

ARTICLE 4 claims 4 theorems

Masses Mass Genesis Master Certificate Stable Closed Mass Genesis Chain From Pay

A machine-checked library of formal theorems has organized its proof that stable patterns of light-like data acquire mass, but the final step remains a declared target, not a completed proof.

Verify this page

The master certificate

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of matching a pattern against that record. The framework's machine-checked library of formal theorems, called Mass Genesis, is the part of the library that connects these abstract patterns to the concept of mass. The declaration named in the question is the top-level certificate for that project: a single structure that exposes the main theorems without forcing other parts of the library to import the long construction details.

The certificate is not marked complete. The library's own documentation states that the active hard target remains the bottom-up derivation of the Q3/Rhat evidence, the CP6/BALANCE geometry, and the selected scalar equation from the framework's primitives for every physically stable pattern. In plain terms, the framework has proved that certain patterns satisfy the mass law, but it has not yet proved that every pattern which should be physically stable actually does so.

What the certificate does establish is a set of conditional theorems. If a pattern is a Q3-closed pattern and its load recognition cost is zero, then the pattern has positive rest mass, its mass is quantized in units of the golden ratio, and its rest mass equals its predicted mass. The same conclusion follows if the pattern is Born-normalized, a condition about the size of its first window. These results are proved in the library, and they are the core of what the certificate exposes.

The certificate also records a deliberate limitation. The library proves that a spatially closed stable pattern does not have to be window-equivariant, meaning that the pattern's structure can be stable in one sense without being stable under the eight-tick cycle. It also proves that a pattern can have zero load recognition cost without having localized support. These are not failures; they are precise statements about what the framework's axioms do and do not force.

What the certificate does not claim is that the mass genesis chain is complete. The bottom-up derivation remains open. The certificate is a stable summary of what has been proved, not a claim that the project is finished.

THEOREM MassGenesisMasterCertificate · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean
MassGenesisMasterCertificate · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean:54876 · truncated 
/-- Audit certificate for the current canonical primitive Mass Genesis surface. -/
structure MassGenesisMasterCertificate where
  hard_target_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
      (∀ k : ℕ,
        integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
      0 < restMass ψ ∧
      PhiRungQuantized ψ ∧
      restMass ψ = predictedMass ψ ∧
      T.readout.inertialMass ψ = restMass ψ ∧
      T.readout.gravitationalMass ψ = restMass ψ
  physical_hard_target_closes_full_chain :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop}
      (T : StableLoadReadoutTheory (Fin 8)),
      CurrentMassGenesisHardTarget PhysicalStable →
      ∀ {ψ : LightPattern (Fin 8)},
        PhysicalStable ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  hard_target_gives_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
      PrimitiveMassGenesisEvidence ψ
  hard_target_gives_bottom_up :
    ∀ {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
      BottomUpAdmissibilityEvidence ψ
  physical_hard_target_gives_admissibility :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      CurrentMassGenesisHardTarget PhysicalStable →
      PhysicalStablePatternsAreMassAdmissible PhysicalStable
  selected_branch_window_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  selected_branch_window_gives_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        restMass ψ = predictedMass ψ
  selected_branch_window_gives_primitive_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        PrimitiveMassGenesisEvidence ψ
  selected_branch_window_gives_bottom_up :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        BottomUpAdmissibilityEvidence ψ
  selected_branch_window_gives_mass_admissible :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        MassAdmissibleStablePattern ψ
  selected_branch_window_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        FullMassGenesisConclusion T ψ
  primitive_dynamics_gives_q3_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        Q3ClosedPatternEvidence ψ
  primitive_dynamics_gives_primitive_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        PrimitiveMassGenesisEvidence ψ
  primitive_dynamics_gives_bottom_up :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        BottomUpAdmissibilityEvidence ψ
  primitive_dynamics_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  primitive_dynamics_gives_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        restMass ψ = predictedMass ψ
  primitive_dynamics_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        FullMassGenesisConclusion T ψ
  stable_closed_primitive_dynamics_target_gives_dynamics :
    StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          PrimitiveMassGenesisDynamics ψ
  stable_closed_primitive_dynamics_target_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8)),
      StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          (∀ k : ℕ,
            integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
          0 < restMass ψ ∧
          PhiRungQuantized ψ ∧
          restMass ψ = predictedMass ψ ∧
          T.readout.inertialMass ψ = restMass ψ ∧
          T.readout.gravitationalMass ψ = restMass ψ
  stable_closed_primitive_dynamics_target_gives_masslaw :
    StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          restMass ψ = predictedMass ψ
  stable_closed_primitive_dynamics_target_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8)),
      StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          FullMassGenesisConclusion T ψ
  refined_stable_predicate_is_primitive_dynamics :
    ∀ {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ ↔ PrimitiveMassGenesisDynamics ψ
  refined_stable_predicate_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  refined_stable_predicate_gives_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ →
        restMass ψ = predictedMass ψ
  refined_stable_predicate_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ →
        FullMassGenesisConclusion T ψ
  refined_stable_predicate_supplies_primitive_dynamics :
    PhysicalStablePatternsHavePrimitiveMassGenesisDynamics
      RefinedMassGenesisStablePattern
  component_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  component_dynamics_closes_refined_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  component_dynamics_gives_refined_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        restMass ψ = predictedMass ψ
  component_dynamics_gives_refined_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        FullMassGenesisConclusion T ψ
  physical_stable_component_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveComponentDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  phase0_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  phase0_tail_dynamics_closes_refined_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  phase0_tail_dynamics_gives_refined_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        restMass ψ = predictedMass ψ
  phase0_tail_dynamics_gives_refined_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        FullMassGenesisConclusion T ψ
  physical_stable_phase0_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHavePhase0TailDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  sqrt_scalar_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisSqrtScalarTailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  inline_sqrt_scalar_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineSqrtScalarTailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  inline_scalar_sign_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  canonical_primitive_target_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
        RefinedMassGenesisStablePattern ψ
  inline_scalar_sign_tail_closes_refined_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  inline_scalar_sign_tail_gives_refined_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        restMass ψ = predictedMass ψ
  inline_scalar_sign_tail_gives_refined_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        FullMassGenesisConclusion T ψ
  physical_stable_sqrt_scalar_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveSqrtScalarTailDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  physical_stable_inline_sqrt_scalar_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveInlineSqrtScalarTailDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  physical_stable_inline_scalar_sign_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveInlineScalarSignTailDynamics PhysicalStable →
        ∀ ψ : LightPattern (

-- … truncated for the page; open the module for the rest.
THEOREM massGenesisOnCarrier_of_loadRecognitionCost_zero · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean
massGenesisOnCarrier_of_loadRecognitionCost_zero · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean:61382 
/-- M1 on the carrier in σ = 0 form: the full Mass Genesis conclusion holds when the
load-ratio recognition cost vanishes. This is route (a)'s closure of the carrier
theorem onto the canonical RS ledger. -/
theorem massGenesisOnCarrier_of_loadRecognitionCost_zero
    (T : StableLoadReadoutTheory (Fin 8))
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hcost : loadRecognitionCost ψ = 0) :
    (∀ k : ℕ,
      integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
    0 < restMass ψ ∧
    PhiRungQuantized ψ ∧
    restMass ψ = predictedMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ :=
  massGenesisOnCarrier_of_loadNormalizedToTopology T ⟨E⟩
    ((loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).1 hcost)
THEOREM spatiallyClosedStable_does_not_force_windowEquivariant · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean
spatiallyClosedStable_does_not_force_windowEquivariant · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean:61125 
/-- **OBSTRUCTION (carrier dynamics, O3 window-residual, sess. 11).** The window-equivariance
hypothesis of `massGenesisOnSpatiallyClosedStable_of_residuals` is genuinely INDEPENDENT of its
spatial-closure source — it cannot be dropped, and no genuine Q3-closure dynamical source supplies it.
The constant pattern on the gap-1 neutral window is a FULL `SpatiallyClosedStablePattern`: its support
is all of `Fin 8` (localized and trivially step-closed, hence `FullEightTickSupport`), it carries
nontrivial neutral load (`normSq8 (neutralize gapOneTwoPhaseMode) = 2 > 0`), and it closes under the
R̂-orbit at period 8 (`cyclicShift_period_8`). Yet it FAILS `EightTickWindowEquivariant`, because every
site carries the SAME window rather than successive `cyclicShift` images, and the gap-1 window is not
R̂-fixed. So the three genuine closure sources combined — R̂-orbit closure (`ClosedRHatOrbit`), spatial
step-closure (`SpatialStepClosedSupport`), and stability — do not force window-equivariance. It is
irreducibly the worldline identification of one site-step with one R̂-tick, a separate dynamical input.
This strengthens the session-8 `fullSupport_does_not_force_windowEquivariant` (which only used full
SITE support) to the full carrier-source predicate. -/
theorem spatiallyClosedStable_does_not_force_windowEquivariant :
    SpatiallyClosedStablePattern (constWindowPattern gapOneTwoPhaseMode) ∧
      ¬ EightTickWindowEquivariant (constWindowPattern gapOneTwoPhaseMode) := by
  refine ⟨⟨⟨?_, ?_, ?_⟩, ?_⟩, fullSupport_does_not_force_windowEquivariant.2⟩
  · exact Finset.univ_nonempty
  · refine ⟨0, Finset.mem_univ _, ?_⟩
    have hneut : neutralize ((constWindowPattern gapOneTwoPhaseMode).window 0)
        = gapOneTwoPhaseMode := by
      funext j
      show gapOneTwoPhaseMode j - (∑ i, gapOneTwoPhaseMode i) / 8 = gapOneTwoPhaseMode j
      rw [gapOneTwoPhaseMode_neutral]; ring
    rw [hneut]
    have hns : normSq8 gapOneTwoPhaseMode = 2 := by
      simp [normSq8, gapOneTwoPhaseMode, Fin.sum_univ_eight, Complex.normSq_apply]; norm_num
    rw [hns]; norm_num
  · exact ⟨8, by norm_num, dvd_refl 8, fun x _ => cyclicShift_period_8 _⟩
  · intro x _; exact Finset.mem_univ _
THEOREM MassGenesisMasterCertificate · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean
MassGenesisMasterCertificate · IndisputableMonolith/Masses/MassGenesis/MasterCertificate.lean:54876 · truncated 
/-- Audit certificate for the current canonical primitive Mass Genesis surface. -/
structure MassGenesisMasterCertificate where
  hard_target_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8)) {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
      (∀ k : ℕ,
        integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
      0 < restMass ψ ∧
      PhiRungQuantized ψ ∧
      restMass ψ = predictedMass ψ ∧
      T.readout.inertialMass ψ = restMass ψ ∧
      T.readout.gravitationalMass ψ = restMass ψ
  physical_hard_target_closes_full_chain :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop}
      (T : StableLoadReadoutTheory (Fin 8)),
      CurrentMassGenesisHardTarget PhysicalStable →
      ∀ {ψ : LightPattern (Fin 8)},
        PhysicalStable ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  hard_target_gives_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
      PrimitiveMassGenesisEvidence ψ
  hard_target_gives_bottom_up :
    ∀ {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
      BottomUpAdmissibilityEvidence ψ
  physical_hard_target_gives_admissibility :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      CurrentMassGenesisHardTarget PhysicalStable →
      PhysicalStablePatternsAreMassAdmissible PhysicalStable
  selected_branch_window_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  selected_branch_window_gives_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        restMass ψ = predictedMass ψ
  selected_branch_window_gives_primitive_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        PrimitiveMassGenesisEvidence ψ
  selected_branch_window_gives_bottom_up :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        BottomUpAdmissibilityEvidence ψ
  selected_branch_window_gives_mass_admissible :
    ∀ {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        MassAdmissibleStablePattern ψ
  selected_branch_window_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
      StableBalancedTopologyRawSelectedBranchWindowComponentData ψ →
        FullMassGenesisConclusion T ψ
  primitive_dynamics_gives_q3_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        Q3ClosedPatternEvidence ψ
  primitive_dynamics_gives_primitive_evidence :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        PrimitiveMassGenesisEvidence ψ
  primitive_dynamics_gives_bottom_up :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        BottomUpAdmissibilityEvidence ψ
  primitive_dynamics_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  primitive_dynamics_gives_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        restMass ψ = predictedMass ψ
  primitive_dynamics_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisDynamics ψ →
        FullMassGenesisConclusion T ψ
  stable_closed_primitive_dynamics_target_gives_dynamics :
    StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          PrimitiveMassGenesisDynamics ψ
  stable_closed_primitive_dynamics_target_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8)),
      StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          (∀ k : ℕ,
            integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
          0 < restMass ψ ∧
          PhiRungQuantized ψ ∧
          restMass ψ = predictedMass ψ ∧
          T.readout.inertialMass ψ = restMass ψ ∧
          T.readout.gravitationalMass ψ = restMass ψ
  stable_closed_primitive_dynamics_target_gives_masslaw :
    StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          restMass ψ = predictedMass ψ
  stable_closed_primitive_dynamics_target_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8)),
      StableClosedPrimitiveDynamicsTarget →
      ∀ {ψ : LightPattern (Fin 8)},
        StableClosedLightPattern ψ →
          FullMassGenesisConclusion T ψ
  refined_stable_predicate_is_primitive_dynamics :
    ∀ {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ ↔ PrimitiveMassGenesisDynamics ψ
  refined_stable_predicate_closes_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  refined_stable_predicate_gives_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ →
        restMass ψ = predictedMass ψ
  refined_stable_predicate_gives_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      RefinedMassGenesisStablePattern ψ →
        FullMassGenesisConclusion T ψ
  refined_stable_predicate_supplies_primitive_dynamics :
    PhysicalStablePatternsHavePrimitiveMassGenesisDynamics
      RefinedMassGenesisStablePattern
  component_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  component_dynamics_closes_refined_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  component_dynamics_gives_refined_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        restMass ψ = predictedMass ψ
  component_dynamics_gives_refined_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisComponentDynamics ψ →
        FullMassGenesisConclusion T ψ
  physical_stable_component_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveComponentDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  phase0_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  phase0_tail_dynamics_closes_refined_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  phase0_tail_dynamics_gives_refined_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        restMass ψ = predictedMass ψ
  phase0_tail_dynamics_gives_refined_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisPhase0TailDynamics ψ →
        FullMassGenesisConclusion T ψ
  physical_stable_phase0_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHavePhase0TailDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  sqrt_scalar_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisSqrtScalarTailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  inline_sqrt_scalar_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineSqrtScalarTailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  inline_scalar_sign_tail_dynamics_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        RefinedMassGenesisStablePattern ψ
  canonical_primitive_target_gives_refined_stable :
    ∀ {ψ : LightPattern (Fin 8)},
      CanonicalPrimitiveMassGenesisTarget ψ →
        RefinedMassGenesisStablePattern ψ
  inline_scalar_sign_tail_closes_refined_full_chain :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        (∀ k : ℕ,
          integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
        0 < restMass ψ ∧
        PhiRungQuantized ψ ∧
        restMass ψ = predictedMass ψ ∧
        T.readout.inertialMass ψ = restMass ψ ∧
        T.readout.gravitationalMass ψ = restMass ψ
  inline_scalar_sign_tail_gives_refined_masslaw :
    ∀ {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        restMass ψ = predictedMass ψ
  inline_scalar_sign_tail_gives_refined_full_conclusion :
    ∀ (T : StableLoadReadoutTheory (Fin 8))
      {ψ : LightPattern (Fin 8)},
      PrimitiveMassGenesisInlineScalarSignTailDynamics ψ →
        FullMassGenesisConclusion T ψ
  physical_stable_sqrt_scalar_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveSqrtScalarTailDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  physical_stable_inline_sqrt_scalar_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveInlineSqrtScalarTailDynamics PhysicalStable →
        ∀ ψ : LightPattern (Fin 8),
          PhysicalStable ψ →
            RefinedMassGenesisStablePattern ψ
  physical_stable_inline_scalar_sign_tail_dynamics_supplies_refined :
    ∀ {PhysicalStable : LightPattern (Fin 8) → Prop},
      PhysicalStablePatternsHaveInlineScalarSignTailDynamics PhysicalStable →
        ∀ ψ : LightPattern (

-- … truncated for the page; open the module for the rest.

What this page does not claim

The certificate does not claim that the mass genesis chain is complete or that all physically stable patterns have been derived from primitives. The certificate does not claim that every pattern with zero load recognition cost has localized support; it proves the opposite. The certificate does not claim that spatial closure alone forces the eight-tick window equivariance condition.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND