Masses Mass Genesis T10 Boolean Anchor Load Ceiling Charged Row Load Normalized

The load ceiling for charged rows

The declaration chargedRow_loadNormalized_settledAnchor_amplitude_gt_four is a proved theorem in the framework's machine-checked library of formal theorems. It concerns a ledger, a discrete record of events, and how much energy a particle's anchor window, the eight-tick interval where its mass is posted, can hold. The theorem states that if a charged row's predicted mass exceeds 256, and its anchor window has a settled shape with amplitude a, then a must be greater than 4. In plain terms: any realized pattern heavy enough to sit on a charged mass row needs thousands of units of amplitude in its anchor window, not the single unit the ledger can post.

The proof is a consequence of two earlier results. First, for any settled anchor window, the predicted mass equals 16 times the square of the amplitude. Second, a Boolean window, one where every tick is either 0, 1, or -1, has a neutralized load of at most 8, a ceiling that is attained exactly by the alternating window. Combining these, a Boolean anchor can only support a predicted mass up to 64. Since every charged row predicts a mass above 256, no charged row's anchor can be Boolean. The theorem's conclusion, that the amplitude exceeds 4, follows directly from the mass formula and the ceiling.

The theorem does not claim that the mass law forbids a Boolean anchor. The normalization condition, LoadNormalizedToTopology, is a definition, not a derived law; the derivation of that condition is an open problem. What the theorem does show is that the normalization condition and a Boolean anchor are jointly unsatisfiable above the ceiling. Whatever derivation eventually supplies the normalization condition, it cannot route through a Boolean posting for any species heavier than 256. The theorem also does not claim that physical matter selects the scale of the witness pattern; the non-vacuity witness is built by rescaling a scale-blind carrier until the normalization equation holds, establishing satisfiability of the hypotheses, not that nature chooses that scale.

The result closes a fork in the campaign's reasoning. Nine attempts looked for a third law to adjudicate between two derived scales: the ledger's Boolean occupancy forces posting amplitude one, while the mass law needs an anchor load of predicted mass divided by 8. The theorem shows no third law is needed. The shape does not fail; a heavy realized pattern may carry a settlement window at its anchor. What fails is the alphabet: only amplitude 1 is a posting, and heavy matter needs thousands of settlements' worth of amplitude in the window where the ledger can post one. The ceiling of 8 is sharp, not an estimate, and it is the maximum over the whole alphabet.

/-- The amplitude a charged fermion's settled anchor would have to post at,
stated as the equation rather than a numeral: above four for every row. -/
theorem chargedRow_loadNormalized_settledAnchor_amplitude_gt_four
    {a : ℝ} {ψ : LightPattern (Fin 8)} {row : ChargedMassRow}
    (hload : LoadNormalizedToTopology ψ)
    (hwin : SettledAnchorWindow a ψ)
    (hmass :
      predictedMass ψ =
        MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row))
    (ha : 0 < a) :
    4 < a := by
  refine loadNormalized_settledAnchor_amplitude_gt_four hload hwin ?_ ha
  rw [hmass]
  exact chargedRow_predict_mass_gt_ceiling row

/-- **The amplitude equation, read off the ceiling's own hypothesis.** A settled
anchor that realizes the mass law's load condition has `predictedMass = 16 a²`.
-/
theorem loadNormalized_settledAnchor_predictedMass_eq
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hload : LoadNormalizedToTopology ψ)
    (hwin : SettledAnchorWindow a ψ) :
    predictedMass ψ = 16 * a ^ 2 := by
  have hsite : normSq8 (neutralize (ψ.window 0)) = predictedMass ψ / 8 :=
    loadNormalizedToTopology_site0_load_eq_predictedMass_div_eight hload
  rw [settledAnchor_neutralizedNormSq hwin] at hsite
  linarith

/-- **The ceiling, sharp.** The neutralized load of a Boolean settlement window
is at most `8`, whatever its shape, because mean subtraction only removes energy
and the alphabet supplies at most one unit per tick. -/
theorem booleanWindow_neutralizedNormSq_le {w : PhotonWindow}
    (hw : BooleanDifferenceSettlementWindow w) :
    normSq8 (neutralize w) ≤ 8 := by
  have hid := normSq8_neutralize_eq w
  have hmean : 0 ≤ Complex.normSq (∑ j : Fin 8, w j) / 8 := by
    have := Complex.normSq_nonneg (∑ j : Fin 8, w j)
    linarith
  have hraw := booleanWindow_normSq8_le_eight hw
  linarith

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

What this page does not claim

The mass law itself is not asserted to be correct. The theorem does not claim that physical matter selects the scale of the witness pattern. No composition or multiplicity law is supplied here.

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: