Species — Recognition explainer

formal statement (Lean)

   9inductive Species
  10  | fermion (f : RSBridge.Fermion)
  11  | W
  12  | Z
  13  | H
  14  deriving DecidableEq, Repr
  15
  16open RSBridge
  17
  18/-- Sector identifier (local copy to avoid circular import).
  19    Note: Neutrino is distinct from Lepton because it has a different baseline (0 vs 2). -/

used by (26)

From the project-wide theorem graph. These declarations reference this one in their body.

ablation_contradictions in IndisputableMonolith.Ablation decl_use
AnchorEq in IndisputableMonolith.Ablation decl_use
anchorEq_implies_Zeq_nonneg in IndisputableMonolith.Ablation decl_use
Z_break6Q in IndisputableMonolith.Ablation decl_use
Z_dropPlus4 in IndisputableMonolith.Ablation decl_use
Z_dropQ4 in IndisputableMonolith.Ablation decl_use
rs_lithium_insight in IndisputableMonolith.Cosmology.Nucleosynthesis decl_use
totalRung_pos in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
Z_life_gt_one in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
sectorOf in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
tildeQ in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
compute_rung in IndisputableMonolith.Masses.RungConstructor.Motif decl_use
compute_rung_sdgt in IndisputableMonolith.Masses.RungConstructor.Motif decl_use
anchor_identity_from_cert in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
equalZ_residue_from_cert in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
Species in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
AnchorCert in IndisputableMonolith.Recognition.Certification decl_use
anchorIdentity_cert in IndisputableMonolith.Recognition.Certification decl_use
anchorIdentity_of_zeroWidthCert in IndisputableMonolith.Recognition.Certification decl_use
equalZ_residue_of_cert in IndisputableMonolith.Recognition.Certification decl_use
Igap in IndisputableMonolith.Recognition.Certification decl_use
M0_pos_of_cert in IndisputableMonolith.Recognition.Certification decl_use
Valid in IndisputableMonolith.Recognition.Certification decl_use
zeroWidthCert in IndisputableMonolith.Recognition.Certification decl_use
zeroWidthCert_valid in IndisputableMonolith.Recognition.Certification decl_use

depends on (24)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Species in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
Lepton in IndisputableMonolith.Physics.AnomalousMoments decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use
RSBridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.RSBridge.Anchor decl_use