Masses Mass Genesis T10 Boolean Anchor Load Ceiling Load Normalized Heavy Settle

The amplitude ceiling

A ledger, a discrete record of events, can post only three values at each tick: plus one, minus one, or zero. The declaration loadNormalized_heavy_settledAnchor_amplitude_gt_two proves that any pattern whose predicted mass exceeds 64, in the framework's units, cannot have an anchor window shaped like a settlement window with amplitude 2 or less. In plain terms: if a realized pattern is heavy enough, the amplitude at its anchor must be greater than 2, so it cannot be a simple posting of one unit.

The proof runs through a chain of equalities. The normalization condition ties the anchor's load to the predicted mass divided by 8. For a settled anchor window, that load equals 16 times the square of the amplitude. Combining these gives predicted mass equals 16 times amplitude squared. If the amplitude were at most 2, the mass would be at most 64, contradicting the hypothesis that it exceeds 64. Therefore the amplitude must be greater than 2.

The result is sharp: the alternating window, which alternates between plus and minus one across the eight ticks, achieves exactly the ceiling load of 8, and hence a mass of 64. No Boolean window can carry more. The theorem is proved in the machine-checked library of formal theorems, with no unproved assumptions. An independent brute-force check of all 6561 possible Boolean windows confirms the maximum is 8, attained at 70 of them.

What the theorem does not claim is that the mass law forbids a Boolean anchor. The normalization condition is a definition, not a derived law; its derivation is an open problem. The theorem only says that the normalization condition and a Boolean anchor are jointly unsatisfiable above the ceiling. It also does not say that physical matter selects the scale that satisfies the normalization; the existence witness is built by rescaling a scale-blind carrier, not by physical selection.

/-- Above the ceiling the required posting amplitude is above two, hence not one,
hence outside the Boolean alphabet by
`settledAnchor_boolean_forces_unitAmplitude`. The constant tracks the ceiling: at
the sharp ceiling `64` the amplitude bound is `2`, and a species above `256`, which
is all of them, gives `4`. -/
theorem loadNormalized_heavy_settledAnchor_amplitude_gt_two
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hload : LoadNormalizedToTopology ψ)
    (hwin : SettledAnchorWindow a ψ)
    (hheavy : 64 < predictedMass ψ)
    (ha : 0 < a) :
    2 < a := by
  have hmass := loadNormalized_settledAnchor_predictedMass_eq hload hwin
  by_contra hle
  push_neg at hle
  nlinarith

/-- **Attainment.** `8` is reached, so the ceiling is the exact maximum of
neutralized load over the Boolean alphabet. -/
theorem booleanWindow_ceiling_attained :
    BooleanDifferenceSettlementWindow alternatingBooleanWindow ∧
      normSq8 (neutralize alternatingBooleanWindow) = 8 := by
  refine ⟨alternatingBooleanWindow_boolean, ?_⟩
  have hsum : (∑ j : Fin 8, alternatingBooleanWindow j) = 0 := by
    simp [alternatingBooleanWindow, Fin.sum_univ_eight]
    norm_num
  rw [normSq8_neutralize_eq, hsum]
  simp [normSq8, alternatingBooleanWindow, Fin.sum_univ_eight]
  norm_num

theorem booleanWindow_sum_norm_le_eight {w : PhotonWindow}
    (hw : BooleanDifferenceSettlementWindow w) :
    ‖∑ j : Fin 8, w j‖ ≤ 8 := by
  calc ‖∑ j : Fin 8, w j‖ ≤ ∑ j : Fin 8, ‖w j‖ := norm_sum_le _ _
    _ ≤ ∑ _j : Fin 8, (1 : ℝ) :=
        Finset.sum_le_sum
          (fun j _ => isBooleanPostingAmplitude_norm_le_one (hw j))
    _ = 8 := by simp

What this page does not claim

The normalization condition is a derived law; it is a definition whose derivation remains open. The theorem says the mass law forbids a Boolean anchor; it only says the normalization condition and a Boolean anchor are jointly unsatisfiable above the ceiling. The existence witness establishes that physical matter selects the scale that satisfies the normalization 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/T10BooleanAnchorLoadCeiling.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: