TauLib · API Book IV

TauLib.BookIV.Particles.SectorAtlas

TauLib.BookIV.Particles.SectorAtlas

Complete sector taxonomy: the map of all 5 sectors with associated particles, force-carrier assignment, sector-particle correspondence table, 9-element canonical generator set, generator adequacy, tau-Yukawa couplings, and the parameter-count comparison (9 generators vs SM’s 19 free parameters).

Registry Cross-References

  • [IV.T80] Exactly Four Primitive Forces (Physical Reading) — exactly_four_primitive_forces

  • [IV.T81] Exactly One Derived Sector — exactly_one_derived_sector

  • [IV.D194] 9-Element Canonical Generator Set — CanonicalGeneratorSet

  • [IV.T82] Generator Adequacy and Minimality — generator_adequacy

  • [IV.D195] τ-Yukawa Coupling — TauYukawaCoupling

  • [IV.R106] Book III template vs Book IV instantiation — comment-only (not_applicable)

  • [IV.R107] Topological rigidity — comment-only (not_applicable)

  • [IV.R108] Yukawa as readout not parameter — yukawa_is_readout

  • [IV.R109] SM parameter count comparison — sm_parameter_comparison

  • [IV.R110] No BSM particles — no_bsm_particles

Mathematical Content

Chapter 45 presents the complete sector atlas: a 13-row table mapping every sector to its force carriers, matter content, and coupling constants. The boundary holonomy algebra H_∂[ω] admits exactly 4 primitive sector characters (D/Gravity, A/Weak, B/EM, C/Strong) and exactly 1 derived sector (ω = B ∩ C = Higgs). The 9 canonical generators (4 vacuum idempotents + 4 gap quanta + 1 crossing generator ι_τ) generate the entire algebra, and no proper subset suffices. The τ-Yukawa couplings are readouts of winding-mode geometry, not free parameters.

Ground Truth Sources

  • Chapter 45 of Book IV (2nd Edition)

Tau.BookIV.Particles.ExactlyFourPrimitive

source structure Tau.BookIV.Particles.ExactlyFourPrimitive :Type

[IV.T80] The boundary holonomy algebra admits exactly four linearly independent primitive sector characters, instantiating at E₁ as:

  • D = Gravity (α-generator)

  • A = Weak (π-generator)

  • B = EM (γ-generator)

  • C = Strong (η-generator)

No fifth primitive sector exists and no GUT unification reduces this count. The four-ness is a topological invariant of L = S¹ ∨ S¹.

  • count : ℕ Number of primitive sectors.

  • sectors : List BookIII.Sectors.Sector Sectors are: D, A, B, C.

  • independent : Bool Each is linearly independent.

  • no_fifth : Bool No fifth sector.

Instances For

Tau.BookIV.Particles.instReprExactlyFourPrimitive

source instance Tau.BookIV.Particles.instReprExactlyFourPrimitive :Repr ExactlyFourPrimitive

Equations

  • Tau.BookIV.Particles.instReprExactlyFourPrimitive = { reprPrec := Tau.BookIV.Particles.instReprExactlyFourPrimitive.repr }

Tau.BookIV.Particles.instReprExactlyFourPrimitive.repr

source def Tau.BookIV.Particles.instReprExactlyFourPrimitive.repr :ExactlyFourPrimitive → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.exactly_four_primitive_forces

source def Tau.BookIV.Particles.exactly_four_primitive_forces :ExactlyFourPrimitive

Equations

  • Tau.BookIV.Particles.exactly_four_primitive_forces = { } Instances For

Tau.BookIV.Particles.four_primitive_count

source theorem Tau.BookIV.Particles.four_primitive_count :exactly_four_primitive_forces.count = 4

Tau.BookIV.Particles.four_primitive_sectors

source theorem Tau.BookIV.Particles.four_primitive_sectors :exactly_four_primitive_forces.sectors.length = 4

Tau.BookIV.Particles.ExactlyOneDerived

source structure Tau.BookIV.Particles.ExactlyOneDerived :Type

[IV.T81] The lemniscate L = S¹ ∨ S¹ has exactly one self-intersection point, so the sector decomposition admits exactly one derived sector: ω = B ∩ C = γ ∩ η (Higgs/mass mechanism).

No other pair of primitive sectors produces a derived sector. This is topologically rigid: any homeomorphism of L preserves the unique wedge point, so the ω-sector cannot be removed.

  • count : ℕ Number of derived sectors.

  • derived : BookIII.Sectors.Sector The derived sector.

  • parent_B : BookIII.Sectors.Sector Parent sectors.

  • parent_C : BookIII.Sectors.Sector Parent sectors.

  • rigid : Bool Topologically rigid.

Instances For

Tau.BookIV.Particles.instReprExactlyOneDerived

source instance Tau.BookIV.Particles.instReprExactlyOneDerived :Repr ExactlyOneDerived

Equations

  • Tau.BookIV.Particles.instReprExactlyOneDerived = { reprPrec := Tau.BookIV.Particles.instReprExactlyOneDerived.repr }

Tau.BookIV.Particles.instReprExactlyOneDerived.repr

source def Tau.BookIV.Particles.instReprExactlyOneDerived.repr :ExactlyOneDerived → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.exactly_one_derived_sector

source def Tau.BookIV.Particles.exactly_one_derived_sector :ExactlyOneDerived

Equations

  • Tau.BookIV.Particles.exactly_one_derived_sector = { } Instances For

Tau.BookIV.Particles.one_derived_count

source theorem Tau.BookIV.Particles.one_derived_count :exactly_one_derived_sector.count = 1

Tau.BookIV.Particles.total_sector_count

source theorem Tau.BookIV.Particles.total_sector_count :exactly_four_primitive_forces.count + exactly_one_derived_sector.count = 5

Total sector count: 4 primitive + 1 derived = 5.

Tau.BookIV.Particles.GeneratorGroup

source inductive Tau.BookIV.Particles.GeneratorGroup :Type

Generator group classification within H_∂[ω].

  • vacuumIdempotent : GeneratorGroup Vacuum idempotent (one per primitive sector).

  • gapQuantum : GeneratorGroup Gap quantum (one per primitive sector).

  • crossingGenerator : GeneratorGroup Crossing generator (unique, ι_τ).

Instances For

Tau.BookIV.Particles.instReprGeneratorGroup.repr

source def Tau.BookIV.Particles.instReprGeneratorGroup.repr :GeneratorGroup → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.instReprGeneratorGroup

source instance Tau.BookIV.Particles.instReprGeneratorGroup :Repr GeneratorGroup

Equations

  • Tau.BookIV.Particles.instReprGeneratorGroup = { reprPrec := Tau.BookIV.Particles.instReprGeneratorGroup.repr }

Tau.BookIV.Particles.instDecidableEqGeneratorGroup

source instance Tau.BookIV.Particles.instDecidableEqGeneratorGroup :DecidableEq GeneratorGroup

Equations

  • Tau.BookIV.Particles.instDecidableEqGeneratorGroup x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Tau.BookIV.Particles.instBEqGeneratorGroup.beq

source def Tau.BookIV.Particles.instBEqGeneratorGroup.beq :GeneratorGroup → GeneratorGroup → Bool

Equations

  • Tau.BookIV.Particles.instBEqGeneratorGroup.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx) Instances For

Tau.BookIV.Particles.instBEqGeneratorGroup

source instance Tau.BookIV.Particles.instBEqGeneratorGroup :BEq GeneratorGroup

Equations

  • Tau.BookIV.Particles.instBEqGeneratorGroup = { beq := Tau.BookIV.Particles.instBEqGeneratorGroup.beq }

Tau.BookIV.Particles.CanonicalGenerator

source structure Tau.BookIV.Particles.CanonicalGenerator :Type

[IV.D194] A canonical generator of the boundary holonomy algebra. The 9 generators come in three groups:

  • 4 sector vacuum idempotents

  • 4 gap quanta (one per sector)

  • 1 crossing generator ι_τ coupling χ₊ and χ₋

  • label : String Generator label.

  • group : GeneratorGroup Group classification.

  • sector : Option BookIII.Sectors.Sector Associated sector (if applicable).

Instances For

Tau.BookIV.Particles.instReprCanonicalGenerator

source instance Tau.BookIV.Particles.instReprCanonicalGenerator :Repr CanonicalGenerator

Equations

  • Tau.BookIV.Particles.instReprCanonicalGenerator = { reprPrec := Tau.BookIV.Particles.instReprCanonicalGenerator.repr }

Tau.BookIV.Particles.instReprCanonicalGenerator.repr

source def Tau.BookIV.Particles.instReprCanonicalGenerator.repr :CanonicalGenerator → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.canonical_generator_set

source def Tau.BookIV.Particles.canonical_generator_set :List CanonicalGenerator

[IV.D194] The 9-element canonical generator set. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.nine_generators

source theorem Tau.BookIV.Particles.nine_generators :canonical_generator_set.length = 9

Tau.BookIV.Particles.GeneratorAdequacy

source structure Tau.BookIV.Particles.GeneratorAdequacy :Type

[IV.T82] The 9 canonical generators generate the entire boundary holonomy algebra H_∂[ω], and no proper subset suffices. Every polynomial expression in these 9 yields a physical observable. Adequacy: span = H_∂[ω]. Minimality: removal of any one breaks span.

  • total : ℕ Total generators.

  • adequate : Bool Adequate: they generate H_∂[ω].

  • minimal : Bool Minimal: no proper subset suffices.

  • all_observable : Bool Every polynomial is a physical observable.

Instances For

Tau.BookIV.Particles.instReprGeneratorAdequacy.repr

source def Tau.BookIV.Particles.instReprGeneratorAdequacy.repr :GeneratorAdequacy → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.instReprGeneratorAdequacy

source instance Tau.BookIV.Particles.instReprGeneratorAdequacy :Repr GeneratorAdequacy

Equations

  • Tau.BookIV.Particles.instReprGeneratorAdequacy = { reprPrec := Tau.BookIV.Particles.instReprGeneratorAdequacy.repr }

Tau.BookIV.Particles.generator_adequacy

source def Tau.BookIV.Particles.generator_adequacy :GeneratorAdequacy

Equations

  • Tau.BookIV.Particles.generator_adequacy = { } Instances For

Tau.BookIV.Particles.adequacy_count

source theorem Tau.BookIV.Particles.adequacy_count :generator_adequacy.total = 9

Tau.BookIV.Particles.is_adequate

source theorem Tau.BookIV.Particles.is_adequate :generator_adequacy.adequate = true

Tau.BookIV.Particles.is_minimal

source theorem Tau.BookIV.Particles.is_minimal :generator_adequacy.minimal = true

Tau.BookIV.Particles.TauYukawaCoupling

source structure Tau.BookIV.Particles.TauYukawaCoupling :Type

[IV.D195] τ-Yukawa coupling: the coupling of a fermion mode χ_{m,n} in sector X to the Higgs sector ω.

y_f = κ(ω) / √(m² + n²·ι_τ²) × Γ_gen(f)

Determined by winding-mode overlap with the ω-sector crossing character. NOT a free parameter — a readout of fiber geometry.

  • fermion : String Fermion name.

  • sector : BookIII.Sectors.Sector Sector.

  • generation : ℕ Generation (1, 2, or 3).

  • coupling_numer : ℕ Approximate coupling (numerator, scaled ×10⁶).

  • coupling_denom : ℕ Coupling denominator.

  • denom_pos : self.coupling_denom > 0 Denominator positive.

  • gen_valid : self.generation ≥ 1 ∧ self.generation ≤ 3 Valid generation.

Instances For

Tau.BookIV.Particles.instReprTauYukawaCoupling.repr

source def Tau.BookIV.Particles.instReprTauYukawaCoupling.repr :TauYukawaCoupling → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.instReprTauYukawaCoupling

source instance Tau.BookIV.Particles.instReprTauYukawaCoupling :Repr TauYukawaCoupling

Equations

  • Tau.BookIV.Particles.instReprTauYukawaCoupling = { reprPrec := Tau.BookIV.Particles.instReprTauYukawaCoupling.repr }

Tau.BookIV.Particles.YukawaReadout

source structure Tau.BookIV.Particles.YukawaReadout :Type

[IV.R108] The Yukawa hierarchy spanning six orders of magnitude (y_e ≈ 3×10⁻⁶ to y_t ≈ 1) is a readout of winding-mode geometry on T², not a set of independent parameters. It arises from compounding three geometric factors, each determined by ι_τ alone.

  • span_orders : ℕ Orders of magnitude span.

  • num_factors : ℕ Number of geometric factors.

  • iota_determined : Bool All determined by ι_τ.

  • not_free : Bool Not free parameters.

Instances For

Tau.BookIV.Particles.instReprYukawaReadout.repr

source def Tau.BookIV.Particles.instReprYukawaReadout.repr :YukawaReadout → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.instReprYukawaReadout

source instance Tau.BookIV.Particles.instReprYukawaReadout :Repr YukawaReadout

Equations

  • Tau.BookIV.Particles.instReprYukawaReadout = { reprPrec := Tau.BookIV.Particles.instReprYukawaReadout.repr }

Tau.BookIV.Particles.yukawa_is_readout

source def Tau.BookIV.Particles.yukawa_is_readout :YukawaReadout

Equations

  • Tau.BookIV.Particles.yukawa_is_readout = { } Instances For

Tau.BookIV.Particles.yukawa_span

source theorem Tau.BookIV.Particles.yukawa_span :yukawa_is_readout.span_orders = 6

Tau.BookIV.Particles.yukawa_not_free

source theorem Tau.BookIV.Particles.yukawa_not_free :yukawa_is_readout.not_free = true

Tau.BookIV.Particles.ParameterComparison

source structure Tau.BookIV.Particles.ParameterComparison :Type

[IV.R109] Parameter count comparison:

  • Standard Model: ~19 free parameters

  • Category τ: 9 canonical generators, of which only 1 (ι_τ) is a numerical constant; the remaining 8 are structural objects uniquely determined by the boundary algebra.

Reduction: 19 free parameters → 1 master constant.

  • sm_params : ℕ SM free parameters.

  • tau_generators : ℕ τ canonical generators.

  • tau_numerical : ℕ Of which numerical constants.

  • tau_structural : ℕ Of which structural (determined by algebra).

Instances For

Tau.BookIV.Particles.instReprParameterComparison

source instance Tau.BookIV.Particles.instReprParameterComparison :Repr ParameterComparison

Equations

  • Tau.BookIV.Particles.instReprParameterComparison = { reprPrec := Tau.BookIV.Particles.instReprParameterComparison.repr }

Tau.BookIV.Particles.instReprParameterComparison.repr

source def Tau.BookIV.Particles.instReprParameterComparison.repr :ParameterComparison → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.sm_parameter_comparison

source def Tau.BookIV.Particles.sm_parameter_comparison :ParameterComparison

Equations

  • Tau.BookIV.Particles.sm_parameter_comparison = { } Instances For

Tau.BookIV.Particles.sm_has_19

source theorem Tau.BookIV.Particles.sm_has_19 :sm_parameter_comparison.sm_params = 19

Tau.BookIV.Particles.tau_one_constant

source theorem Tau.BookIV.Particles.tau_one_constant :sm_parameter_comparison.tau_numerical = 1

Tau.BookIV.Particles.structural_plus_numerical

source theorem Tau.BookIV.Particles.structural_plus_numerical :sm_parameter_comparison.tau_structural + sm_parameter_comparison.tau_numerical = sm_parameter_comparison.tau_generators

Tau.BookIV.Particles.NoBSM

source structure Tau.BookIV.Particles.NoBSM :Type

[IV.R110] The periodic table of τ-particles contains no BSM particles: no supersymmetric partners, no leptoquarks, no right-handed neutrinos, no fourth generation, no dark matter candidates with new quantum numbers. This is a structural consequence of the Exactly-Four Theorem and lemniscate topology.

  • no_susy : Bool No supersymmetry.

  • no_leptoquarks : Bool No leptoquarks.

  • no_rh_neutrinos : Bool No right-handed neutrinos.

  • no_fourth_gen : Bool No fourth generation.

  • no_new_dm : Bool No new dark matter candidates.

Instances For

Tau.BookIV.Particles.instReprNoBSM.repr

source def Tau.BookIV.Particles.instReprNoBSM.repr :NoBSM → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.instReprNoBSM

source instance Tau.BookIV.Particles.instReprNoBSM :Repr NoBSM

Equations

  • Tau.BookIV.Particles.instReprNoBSM = { reprPrec := Tau.BookIV.Particles.instReprNoBSM.repr }

Tau.BookIV.Particles.no_bsm_particles

source def Tau.BookIV.Particles.no_bsm_particles :NoBSM

Equations

  • Tau.BookIV.Particles.no_bsm_particles = { } Instances For

Tau.BookIV.Particles.bsm_all_excluded

source theorem Tau.BookIV.Particles.bsm_all_excluded :no_bsm_particles.no_susy = true ∧ no_bsm_particles.no_leptoquarks = true ∧ no_bsm_particles.no_rh_neutrinos = true ∧ no_bsm_particles.no_fourth_gen = true ∧ no_bsm_particles.no_new_dm = true

Tau.BookIV.Particles.AtlasEntry

source structure Tau.BookIV.Particles.AtlasEntry :Type

An entry in the 13-row sector atlas table.

  • label : String Row label.

  • sector : BookIII.Sectors.Sector Sector.

  • carrier : String Force carrier(s).

  • matter : String Matter content.

Instances For

Tau.BookIV.Particles.instReprAtlasEntry.repr

source def Tau.BookIV.Particles.instReprAtlasEntry.repr :AtlasEntry → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.instReprAtlasEntry

source instance Tau.BookIV.Particles.instReprAtlasEntry :Repr AtlasEntry

Equations

  • Tau.BookIV.Particles.instReprAtlasEntry = { reprPrec := Tau.BookIV.Particles.instReprAtlasEntry.repr }

Tau.BookIV.Particles.sector_atlas

source def Tau.BookIV.Particles.sector_atlas :List AtlasEntry

The sector atlas: complete mapping from sectors to physical content. This is the E₁ instantiation of Book III’s abstract template. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIV.Particles.atlas_five_entries

source theorem Tau.BookIV.Particles.atlas_five_entries :sector_atlas.length = 5