theorem proved term proof

`N_sec_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  85theorem N_sec_eq : N_sec = 4 := by unfold N_sec D; norm_num

proof body

Term-mode proof.

  86
  87/-! ## Lepton Sector Geometry (DERIVED, not hardcoded) -/
  88
  89/-- Lepton sector binary gauge: B = -(bilateral × E_passive) = -22.
  90    The bilateral factor (= 2) comes from reciprocal pairing (Tr4). -/

depends on (12)

Lean names referenced from this declaration's body.

reciprocal in IndisputableMonolith.Algebra.CostAlgebra decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
reciprocal in IndisputableMonolith.Foundation.LedgerForcing decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
E_passive in IndisputableMonolith.Masses.Anchor decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
Sector in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
Lepton in IndisputableMonolith.Physics.AnomalousMoments decl_use
N_sec in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
E_passive in IndisputableMonolith.Physics.MassTopology decl_use
Sector in IndisputableMonolith.RSBridge.Anchor decl_use