Encyclopedia Masses Masses Mass Genesis T10 Boolean Anchor Ratio Wall Boolean Anchor Predicted Mass

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Boolean Anchor Ratio Wall Boolean Anchor Predicted Mass

A single theorem pins any Boolean-anchored predicted mass between 1 and 64, a bound that survives every change of mass unit.

Verify this page

The Boolean anchor bound

In the Recognition Science framework, a ledger (a discrete record of events) can be posted with different alphabets. One alphabet, the Boolean posting alphabet, allows each tick to be only +1, 0, or -1. The declaration booleanAnchor_predictedMass_mem_Icc proves a sharp consequence: if a pattern's load is normalized to the topology and its predicted mass is positive, then that mass lies between 1 and 64, inclusive. The proof runs through the load formula N - S²/8, where N is the number of occupied ticks and S their signed sum. Because both are integers, the load is a multiple of an eighth, so it is either zero or at least 1/8. That positive floor, combined with a ceiling of 8, bounds the ratio of any two such loads.

The bound matters because it is unit-free. Rescaling the mass unit by any positive factor k cancels in a ratio, so the factor-of-64 gap between two Boolean-anchored masses cannot be closed by changing units. This turns a threshold statement ("the anchor is capped at 64") into a ratio statement with real strength. The theorem is part of a machine-checked library of formal theorems, and it is what a later wall uses: the electron and muon, eleven rungs apart in the same sector, have a predicted-mass ratio of phi^11, which exceeds 144. A Boolean anchor allows at most 64, so the required ratio exceeds the achievable one by a factor better than two.

What the theorem does not claim is as precise as what it proves. It does not say the Boolean alphabet is the actual carrier of the anchor load for the species table; it only excludes that alphabet under the stated normalization. It does not address composite postings at rational multiplicity, which are unbounded and dense. It does not show what the anchor is, and it does not compare a mass against a threshold in an imported unit. The theorem is a conditional exclusion, not an identification.

THEOREM booleanAnchor_predictedMass_mem_Icc · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
booleanAnchor_predictedMass_mem_Icc · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:126 
/-- **Both ends at once.** Under the normalization condition a Boolean anchor
with nonzero load carries a predicted mass between `1` and `64`. -/
theorem booleanAnchor_predictedMass_mem_Icc
    {ψ : LightPattern (Fin 8)}
    (hbool : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hload : LoadNormalizedToTopology ψ)
    (hpos : 0 < predictedMass ψ) :
    1 ≤ predictedMass ψ ∧ predictedMass ψ ≤ 64 := by
  have hsite : normSq8 (neutralize (ψ.window 0)) = predictedMass ψ / 8 :=
    loadNormalizedToTopology_site0_load_eq_predictedMass_div_eight hload
  have hsitepos : 0 < normSq8 (neutralize (ψ.window 0)) := by
    rw [hsite]; linarith
  have hlow := booleanWindow_load_pos_ge_eighth hbool hsitepos
  have hhigh := booleanWindow_neutralizedNormSq_le hbool
  rw [hsite] at hlow hhigh
  constructor <;> linarith
THEOREM booleanWindow_load_pos_ge_eighth · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
booleanWindow_load_pos_ge_eighth · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:103 
/-- **A Boolean load is zero or at least an eighth.** The floor is what
distinguishes this alphabet from the dense composite-posting family: an integer
numerator over eight cannot be positive and arbitrarily small. -/
theorem booleanWindow_load_pos_ge_eighth {w : PhotonWindow}
    (hw : BooleanDifferenceSettlementWindow w)
    (hpos : 0 < normSq8 (neutralize w)) :
    1 / 8 ≤ normSq8 (neutralize w) := by
  obtain ⟨N, S, hform⟩ := booleanWindow_load_int_form hw
  rw [hform] at hpos ⊢
  -- `8 N - S ^ 2` is a positive integer, hence at least one.
  have hint : (0 : ℤ) < 8 * N - S ^ 2 := by
    by_contra hle
    push_neg at hle
    have : ((8 * N - S ^ 2 : ℤ) : ℝ) ≤ 0 := by exact_mod_cast hle
    push_cast at this
    linarith
  have hone : (1 : ℤ) ≤ 8 * N - S ^ 2 := hint
  have : (1 : ℝ) ≤ ((8 * N - S ^ 2 : ℤ) : ℝ) := by exact_mod_cast hone
  push_cast at this
  linarith
THEOREM boolean_anchored_mass_ratio_le_sixtyfour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
boolean_anchored_mass_ratio_le_sixtyfour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:143 
/-- **The ratio bound, which is the unit-free statement.** Two Boolean-anchored
patterns satisfying the normalization condition have predicted masses within a
factor of `64`, and rescaling the mass unit by any positive `k` cannot change
that, because `k` cancels. -/
theorem boolean_anchored_mass_ratio_le_sixtyfour
    {ψ χ : LightPattern (Fin 8)} {k : ℝ} (hk : 0 < k)
    (hbψ : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hbχ : BooleanDifferenceSettlementWindow (χ.window 0))
    (hlψ : LoadNormalizedToTopology ψ) (hlχ : LoadNormalizedToTopology χ)
    (hpψ : 0 < predictedMass ψ) (hpχ : 0 < predictedMass χ) :
    k * predictedMass χ ≤ 64 * (k * predictedMass ψ) := by
  obtain ⟨hψ1, _⟩ := booleanAnchor_predictedMass_mem_Icc hbψ hlψ hpψ
  obtain ⟨_, hχ64⟩ := booleanAnchor_predictedMass_mem_Icc hbχ hlχ hpχ
  nlinarith
THEOREM phi_zpow_eleven_gt_oneFortyFour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
phi_zpow_eleven_gt_oneFortyFour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:160 
/-- `phi ^ 11 = 89 phi + 55`, hence above `144`. Only `1 < phi` is needed. -/
theorem phi_zpow_eleven_gt_oneFortyFour : (144 : ℝ) < Constants.phi ^ (11 : ℤ) := by
  have hfib := Constants.PhiLadder.phi_zpow_eq_fib (11 : ℤ)
  have h11 : Int.fib 11 = 89 := by decide
  have h10 : Int.fib (11 - 1) = 55 := by decide
  rw [h11, h10] at hfib
  have hphi : (1 : ℝ) < Constants.phi := Constants.one_lt_phi
  rw [hfib]
  push_cast
  linarith

What this page does not claim

The Boolean alphabet is the actual carrier of the anchor load for the species table. Composite postings at rational multiplicity are excluded by this theorem. The theorem identifies what the anchor is.

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