Encyclopedia Masses Masses Mass Genesis T10 Unit Boolean Charged Sigma Zero Wall

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Unit Boolean Charged Sigma Zero Wall

A machine-checked proof shows that charged particles cannot be read as simple unit settlements, drawing a sharp boundary in the framework's mass theory.

Verify this page

The sigma-zero wall

In the Recognition Science framework, a ledger is a discrete record of recognition events, and each particle species is modeled as a pattern of such events. The framework's mass law assigns each pattern a predicted mass on a phi-power ladder. A special state called sigma-zero occurs when the recognition cost, the price the ledger pays to record the pattern, vanishes exactly. The T10 module asks a precise question: can a charged particle, such as an electron or quark, occupy this sigma-zero state when the ledger is read as a simple unit settlement, one event per tick?

The answer is no, and the framework proves it as a theorem. On a unit settled carrier, sigma-zero holds if and only if the predicted mass is exactly 16. The electron's predicted mass already exceeds 256, and every other charged row in the standard table sits far above that. The gap-one worldline, a pattern with a single missing tick, also fails the mass-16 test. So no named charged topology can be sigma-zero under a unit Boolean reading. The proof is machine-checked in the framework's library of formal theorems, with no unproved assumptions added.

The wall sharpens a known residual. The framework does not yet prove that a settled load is always posted as a load, a statement called SettledLoadIsPostedLoad. What T10 shows is narrower: if that posting happens, it cannot happen at the sigma-zero scale for charged matter. The remaining open doors are multi-quantum occupation equal to the topology factor amplitude, or a LightPattern built from emission by a law other than window-equality settled readout.

The consequence is a boundary condition for the mass theory. Any future derivation of charged particle masses must either use a scaled occupation, not a unit settlement, or find a new reading law. The wall does not say which path is correct; it rules one path out and leaves the others open.

THEOREM unitSettled_sigmaZero_iff_predictedMass_eq_sixteen · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean
unitSettled_sigmaZero_iff_predictedMass_eq_sixteen · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean:67 
/-- **Characterization.** On a unit settled Q3 carrier, vanishing load cost
holds iff the topology predicted mass is exactly `16`. -/
theorem unitSettled_sigmaZero_iff_predictedMass_eq_sixteen
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hunit : SettledAnchorWindow 1 ψ) :
    loadRecognitionCost ψ = 0 ↔ predictedMass ψ = 16 := by
  have hamp :=
    unitSettled_loadRecognitionCost_zero_iff_topologyAmplitude E hunit
  have hsq := factorAmplitude_sq_eq_predictedMass_div_sixteen ψ
  have hnonneg := primitivePositiveStationaryFactorAmplitude_nonneg ψ
  constructor
  · intro hcost
    have hfactor : (1 : ℝ) = primitivePositiveStationaryFactorAmplitude ψ :=
      hamp.1 hcost
    have h1 : (1 : ℝ) = predictedMass ψ / 16 := by
      have : (1 : ℝ) ^ 2 = predictedMass ψ / 16 := by
        rw [hfactor, hsq]
      simpa using this
    have h16 : (16 : ℝ) ≠ 0 := by norm_num
    field_simp [h16] at h1
    linarith
  · intro hmass
    have hfactor_sq :
        primitivePositiveStationaryFactorAmplitude ψ ^ 2 = 1 := by
      rw [hsq, hmass]; norm_num
    have hfactor : primitivePositiveStationaryFactorAmplitude ψ = 1 := by
      rcases (sq_eq_one_iff.mp hfactor_sq) with h1 | hneg
      · exact h1
      · linarith [hnonneg, hneg]
    exact hamp.2 hfactor.symm
THEOREM chargedRow_predict_mass_gt_ceiling · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean
chargedRow_predict_mass_gt_ceiling · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean:454 
/-- **Every charged row is above the Boolean anchor load ceiling.** The lightest
species in the table, the electron, already exceeds `256`; the seeds are between
`10^4` and `10^5`. Consumed by the ceiling module to rule out a Boolean anchor
for the whole charged spectrum rather than for an abstract heavy pattern. -/
theorem chargedRow_predict_mass_gt_ceiling (row : ChargedMassRow) :
    (256 : ℝ) <
      MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row) := by
  have hZ := rowZ_pos row
  cases row with
  | electron =>
      exact lepton_predict_mass_gt_of_seed 2 _ (by decide) hZ lepton_seed_gt_ceiling
  | muon =>
      exact lepton_predict_mass_gt_of_seed 13 _ (by decide) hZ lepton_seed_gt_ceiling
  | tau =>
      exact lepton_predict_mass_gt_of_seed 19 _ (by decide) hZ lepton_seed_gt_ceiling
  | up => exact up_predict_mass_gt_of_seed 4 _ (by decide) hZ up_seed_gt_ceiling
  | charm => exact up_predict_mass_gt_of_seed 17 _ (by decide) hZ up_seed_gt_ceiling
  | top => exact up_predict_mass_gt_of_seed 28 _ (by decide) hZ up_seed_gt_ceiling
  | down => exact down_predict_mass_gt_of_seed 4 _ (by decide) hZ down_seed_gt_ceiling
  | strange =>
      exact down_predict_mass_gt_of_seed 10 _ (by decide) hZ down_seed_gt_ceiling
  | bottom =>
      exact down_predict_mass_gt_of_seed 18 _ (by decide) hZ down_seed_gt_ceiling
THEOREM unitSettled_chargedRowMass_not_sigmaZero · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean
unitSettled_chargedRowMass_not_sigmaZero · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean:489 
/-- If a unit settled Q3 carrier carries a charged-row mass law value, it cannot
be sigma-zero. -/
theorem unitSettled_chargedRowMass_not_sigmaZero
    {ψ : LightPattern (Fin 8)} {row : ChargedMassRow}
    (E : Q3ClosedPatternEvidence ψ)
    (hunit : SettledAnchorWindow 1 ψ)
    (hmass :
      predictedMass ψ =
        MassLaw.predict_mass (rowSector row) (rowRung row) (rowZ row)) :
    loadRecognitionCost ψ ≠ 0 := by
  intro hcost
  have h16 :=
    (unitSettled_sigmaZero_iff_predictedMass_eq_sixteen E hunit).1 hcost
  exact chargedRow_predict_mass_ne_sixteen row (hmass.symm ▸ h16)
THEOREM gapOne_predictedMass_ne_sixteen · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean
gapOne_predictedMass_ne_sixteen · IndisputableMonolith/Masses/MassGenesis/T10UnitBooleanChargedSigmaZeroWall.lean:171 
theorem gapOne_predictedMass_ne_sixteen :
    predictedMass (worldlinePattern gapOneTwoPhaseMode) ≠ 16 := by
  obtain ⟨hsec, hrung, hZ⟩ := worldlineGapOne_sector_rung_Z'
  intro heq
  have hdiv8 : predictedMass (worldlinePattern gapOneTwoPhaseMode) / 8 = 2 := by
    rw [heq]; norm_num
  have htop :
      MassLaw.predict_mass Anchor.Sector.Electroweak 0 0 / 8 = 2 := by
    simpa [predictedMass, hsec, hrung, hZ] using hdiv8
  have hφ :
      Constants.phi ^ (42 : ℕ) / 4 = 2 := by
    rw [← electroweak_rung0_predictedMass_div_eight_eq', htop]
  have hφ' : Constants.phi ^ (42 : ℕ) = (8 : ℝ) := by
    have h4 : (4 : ℝ) ≠ 0 := by norm_num
    field_simp at hφ
    linarith
  exact lt_irrefl (8 : ℝ) (hφ' ▸ phi_pow_fortyTwo_gt_eight')

What this page does not claim

This module does not prove SettledLoadIsPostedLoad. It does not derive the value of any charged particle mass. It does not rule out sigma-zero for charged matter under a multi-quantum reading.

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