Encyclopedia Masses Masses Mass Genesis R4 Genesis Route Cdscratch Boolean Settled Anchor Window Not

ARTICLE 4 claims 4 theorems

Masses Mass Genesis R4 Genesis Route Cdscratch Boolean Settled Anchor Window Not

A machine-checked theorem shows that one proposed condition for admitting matter patterns cannot be determined by the discrete data alone, ruling out a hoped-for shortcut to mass generation.

Verify this page

The anchor window outside the class

In the Recognition Science framework, a ledger (a discrete record of events) admits certain patterns as matter carriers. A proposed admission rule, called BooleanSettledAnchorWindow, would accept a pattern only if a specific boolean occupancy flag is set. The theorem booleanSettledAnchorWindow_not_carrierCertificateGenesis proves that this rule is not determined by the carrier certificate: the set of discrete and relational fields (support, topology, stability, eight-tick support, window equivariance) that the library actually uses to admit patterns. Two patterns can share all those fields yet disagree on the boolean flag, so the rule cannot be expressed as a function of the certificate alone.

The proof works by contradiction. If the rule were certificate-determined, a proved corollary would force it to be invariant under rescaling of the pattern. But the boolean occupancy flag is not rescaling-closed: scaling a pattern can change the flag. The contradiction establishes the theorem. This is a negative result in the framework's mass-genesis program: it closes off one route toward forcing a target normalization, LoadNormalizedToTopology, from creation-side conditions alone.

The theorem does not claim that the boolean rule is false, only that it is not certificate-determined. It also does not claim that no admission rule can force the target; it shows that no rule in the certificate class can. The class itself is non-vacuous: the concrete carrier Q3MatterCarrier is in it and does real work, while the target and the boolean rule are both outside it. The result is a boundary marker, not a dead end.

THEOREM booleanSettledAnchorWindow_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
booleanSettledAnchorWindow_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:311 
/-- `BooleanSettledAnchorWindow` is also outside the class (second control,
matching the banked scope statement of `T10OrbitSectionNoGo`). -/
theorem booleanSettledAnchorWindow_not_carrierCertificateGenesis :
    ¬ IsCarrierCertificateGenesisCondition BooleanSettledAnchorWindow := by
  intro hG
  -- If it were certificate-determined, scale-invariance would follow, but
  -- Boolean occupancy is not rescaling-closed.
  have hscale :
      IsRescalingClosedPatternPredicate BooleanSettledAnchorWindow :=
    fun c hc ψ hψ =>
      (carrierCertificateGenesis_scaleInvariant BooleanSettledAnchorWindow hG hc ψ).mp
        hψ
  exact booleanSettledAnchorWindow_not_rescalingClosed hscale
THEOREM carrierCertificateGenesis_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
carrierCertificateGenesis_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:209 
/-- **Proved corollary (not the definition):** every carrier-certificate genesis
condition is scale-invariant. -/
theorem carrierCertificateGenesis_scaleInvariant
    (G : LightPattern (Fin 8) → Prop)
    (hG : IsCarrierCertificateGenesisCondition G)
    {c : ℝ} (hc : 0 < c) (ψ : LightPattern (Fin 8)) :
    G ψ ↔ G (scalePattern c ψ) :=
  hG ψ (scalePattern c ψ) (carrierCertificateEq_scalePattern hc ψ)
THEOREM carrierCertificateGenesis_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
carrierCertificateGenesis_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:209 
/-- **Proved corollary (not the definition):** every carrier-certificate genesis
condition is scale-invariant. -/
theorem carrierCertificateGenesis_scaleInvariant
    (G : LightPattern (Fin 8) → Prop)
    (hG : IsCarrierCertificateGenesisCondition G)
    {c : ℝ} (hc : 0 < c) (ψ : LightPattern (Fin 8)) :
    G ψ ↔ G (scalePattern c ψ) :=
  hG ψ (scalePattern c ψ) (carrierCertificateEq_scalePattern hc ψ)
THEOREM q3MatterCarrier_isCarrierCertificateGenesis · loadNormalizedToTopology_not_carrierCertificateGenesis · booleanSettledAnchorWindow_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
q3MatterCarrier_isCarrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:257 
/-- Concrete instance: `Q3MatterCarrier` itself cannot force the target. -/
theorem q3MatterCarrier_isCarrierCertificateGenesis :
    IsCarrierCertificateGenesisCondition Q3MatterCarrier := by
  intro ψ χ h
  constructor
  · intro ⟨E⟩
    refine ⟨⟨?_, ?_, ?_⟩⟩
    · exact h.2.2.1.mp E.stable
    · exact h.2.2.2.1.mp E.full_support
    · exact h.2.2.2.2.mp E.window_equivariant
  · intro ⟨E⟩
    refine ⟨⟨?_, ?_, ?_⟩⟩
    · exact h.2.2.1.mpr E.stable
    · exact h.2.2.2.1.mpr E.full_support
    · exact h.2.2.2.2.mpr E.window_equivariant
loadNormalizedToTopology_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:283 
/-- `LoadNormalizedToTopology` is outside the class: the ground state and its
double share a carrier certificate (both are Q3 carriers with the same support
and topology) but disagree on the target. -/
theorem loadNormalizedToTopology_not_carrierCertificateGenesis :
    ¬ IsCarrierCertificateGenesisCondition LoadNormalizedToTopology := by
  intro hG
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hground⟩ := exists_scale_loadNormalizedToTopology Eseed
  let ground := scalePattern c (worldlinePattern gapOneTwoPhaseMode)
  let χ := scalePattern 2 ground
  have Eground : Q3ClosedPatternEvidence ground :=
    scalePattern_q3ClosedEvidence c hc Eseed
  have Eχ : Q3ClosedPatternEvidence χ :=
    scalePattern_q3ClosedEvidence 2 (by norm_num) Eground
  have hcert : CarrierCertificateEq ground χ := by
    simpa [χ] using carrierCertificateEq_scalePattern (by norm_num : (0 : ℝ) < 2) ground
  have hχ : LoadNormalizedToTopology χ := (hG ground χ hcert).mp hground
  have hratio : loadTopologyRatio χ = 4 := by
    have hratio0 : loadTopologyRatio ground = 1 :=
      (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ground).2 hground
    calc
      loadTopologyRatio χ = (2 : ℝ) ^ 2 * loadTopologyRatio ground := by
        simpa [χ] using loadTopologyRatio_scalePattern 2 ground
      _ = 4 := by rw [hratio0]; norm_num
  have hone : loadTopologyRatio χ = 1 :=
    (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology χ).2 hχ
  exact (by norm_num : (4 : ℝ) ≠ 1) (hratio.symm.trans hone)
booleanSettledAnchorWindow_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:311 
/-- `BooleanSettledAnchorWindow` is also outside the class (second control,
matching the banked scope statement of `T10OrbitSectionNoGo`). -/
theorem booleanSettledAnchorWindow_not_carrierCertificateGenesis :
    ¬ IsCarrierCertificateGenesisCondition BooleanSettledAnchorWindow := by
  intro hG
  -- If it were certificate-determined, scale-invariance would follow, but
  -- Boolean occupancy is not rescaling-closed.
  have hscale :
      IsRescalingClosedPatternPredicate BooleanSettledAnchorWindow :=
    fun c hc ψ hψ =>
      (carrierCertificateGenesis_scaleInvariant BooleanSettledAnchorWindow hG hc ψ).mp
        hψ
  exact booleanSettledAnchorWindow_not_rescalingClosed hscale

What this page does not claim

The theorem does not claim that BooleanSettledAnchorWindow is false, only that it is not certificate-determined. The theorem does not claim that no admission rule can force LoadNormalizedToTopology, only that no rule in the certificate class can.

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/R4GenesisRouteCDScratch.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