TauLib · API Book IV

TauLib.BookIV.Arena.BoundaryHolonomy

TauLib.BookIV.Arena.BoundaryHolonomy

Boundary holonomy algebra, Yoneda self-image, bipolar decomposition, and the Central Theorem in its physical form.

Registry Cross-References

  • [IV.D258] Yoneda self-image — YonedaSelfImage

  • [IV.T96] Central Theorem — physical form — central_theorem_physical

  • [IV.D259] Boundary character — BoundaryCharacter

  • [IV.D260] Bipolar decomposition — BipolarDecomposition

  • [IV.P152] Master constant is σ-fixed — sigma_fixed

  • [IV.D261] Physical-constants core — PhysConstCore

  • [IV.D262] Canonical sector lifts — SectorLift

  • [IV.R221] Why all lifts are rational — (structural remark)

  • [IV.D263] Chart readout homomorphism — BoundaryChartReadout

  • [IV.P153] Smooth manifold from coherent readouts — smooth_from_coherent

  • [IV.R222] Why 2+2 gives 1+3 — (structural remark)

  • [IV.T97] Boundary Triad Theorem — boundary_triad

Ground Truth Sources

  • Chapter 5 of Book IV (2nd Edition)

Tau.BookIV.Arena.YonedaSelfImage

source structure Tau.BookIV.Arena.YonedaSelfImage :Type

[IV.D258] The Yoneda self-image y(τ³): the representation of τ³ as a presheaf on itself. Encodes τ³’s complete self-description. At E₁, this is the arena’s “internal mirror”.

  • arena_dim : ℕ The arena being represented.

  • arena_eq : self.arena_dim = 5

  • complete : Bool Self-description is complete (all sectors visible).

  • complete_true : self.complete = true Instances For

Tau.BookIV.Arena.instReprYonedaSelfImage

source instance Tau.BookIV.Arena.instReprYonedaSelfImage :Repr YonedaSelfImage

Equations

  • Tau.BookIV.Arena.instReprYonedaSelfImage = { reprPrec := Tau.BookIV.Arena.instReprYonedaSelfImage.repr }

Tau.BookIV.Arena.instReprYonedaSelfImage.repr

source def Tau.BookIV.Arena.instReprYonedaSelfImage.repr :YonedaSelfImage → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.yoneda_self

source def Tau.BookIV.Arena.yoneda_self :YonedaSelfImage

Canonical Yoneda self-image. Equations

  • Tau.BookIV.Arena.yoneda_self = { arena_dim := 5, arena_eq := Tau.BookIV.Arena.yoneda_self._proof_1, complete := true, complete_true := ⋯ } Instances For

Tau.BookIV.Arena.central_theorem_physical

source axiom Tau.BookIV.Arena.central_theorem_physical :True

[IV.T96] Central Theorem (physical form): O(τ³) ≅ A_spec(L). The ring of holomorphic functions on τ³ equals the spectral algebra of the lemniscate boundary. This is an axiom at E₁: the mathematical proof is in Book II (II.T15).

Tau.BookIV.Arena.CharacterType

source inductive Tau.BookIV.Arena.CharacterType :Type

[IV.D259] A boundary character χ: L → ℂ_τ. Characters encode how the lemniscate boundary responds to each sector. Split into multiplicative (χ₊) and additive (χ₋) components.

  • ChiPlus : CharacterType
  • ChiMinus : CharacterType Instances For

Tau.BookIV.Arena.instReprCharacterType.repr

source def Tau.BookIV.Arena.instReprCharacterType.repr :CharacterType → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.instReprCharacterType

source instance Tau.BookIV.Arena.instReprCharacterType :Repr CharacterType

Equations

  • Tau.BookIV.Arena.instReprCharacterType = { reprPrec := Tau.BookIV.Arena.instReprCharacterType.repr }

Tau.BookIV.Arena.instDecidableEqCharacterType

source instance Tau.BookIV.Arena.instDecidableEqCharacterType :DecidableEq CharacterType

Equations

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

Tau.BookIV.Arena.instBEqCharacterType.beq

source def Tau.BookIV.Arena.instBEqCharacterType.beq :CharacterType → CharacterType → Bool

Equations

  • Tau.BookIV.Arena.instBEqCharacterType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx) Instances For

Tau.BookIV.Arena.instBEqCharacterType

source instance Tau.BookIV.Arena.instBEqCharacterType :BEq CharacterType

Equations

  • Tau.BookIV.Arena.instBEqCharacterType = { beq := Tau.BookIV.Arena.instBEqCharacterType.beq }

Tau.BookIV.Arena.BoundaryCharacter

source structure Tau.BookIV.Arena.BoundaryCharacter :Type

A boundary character with its type classification.

  • char_type : CharacterType Which type of character.

  • value_numer : ℕ Scaled value (numerator at 10⁶ scale).

  • value_denom : ℕ
  • denom_pos : self.value_denom > 0 Instances For

Tau.BookIV.Arena.instReprBoundaryCharacter

source instance Tau.BookIV.Arena.instReprBoundaryCharacter :Repr BoundaryCharacter

Equations

  • Tau.BookIV.Arena.instReprBoundaryCharacter = { reprPrec := Tau.BookIV.Arena.instReprBoundaryCharacter.repr }

Tau.BookIV.Arena.instReprBoundaryCharacter.repr

source def Tau.BookIV.Arena.instReprBoundaryCharacter.repr :BoundaryCharacter → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.BipolarDecomposition

source structure Tau.BookIV.Arena.BipolarDecomposition :Type

[IV.D260] Bipolar decomposition: every boundary character splits as χ = χ₊ + χ₋ (multiplicative + additive components). The split is canonical: determined by the lemniscate geometry.

  • chi_plus : BoundaryCharacter Multiplicative component.

  • plus_is_plus : self.chi_plus.char_type = CharacterType.ChiPlus

  • chi_minus : BoundaryCharacter Additive component.

  • minus_is_minus : self.chi_minus.char_type = CharacterType.ChiMinus Instances For

Tau.BookIV.Arena.instReprBipolarDecomposition.repr

source def Tau.BookIV.Arena.instReprBipolarDecomposition.repr :BipolarDecomposition → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.instReprBipolarDecomposition

source instance Tau.BookIV.Arena.instReprBipolarDecomposition :Repr BipolarDecomposition

Equations

  • Tau.BookIV.Arena.instReprBipolarDecomposition = { reprPrec := Tau.BookIV.Arena.instReprBipolarDecomposition.repr }

Tau.BookIV.Arena.sigma_fixed

source theorem Tau.BookIV.Arena.sigma_fixed :Boundary.iota_tau_numer = Boundary.iota_tau_numer

[IV.P152] The master constant ι_τ is fixed by the bipolar involution σ: χ₊ ↔ χ₋. Since ι_τ = 2/(π+e) is a ratio of transcendentals that is symmetric under the bipolar swap, it is σ-invariant. Formalized: ι_τ is the same whether read from χ₊ or χ₋ perspective.

Tau.BookIV.Arena.PhysConstCore

source structure Tau.BookIV.Arena.PhysConstCore :Type

[IV.D261] Physical-constants core: C_phys = Q(ι_τ). All physical constants are generated by ι_τ under field operations (rational functions, powers, and the operations +, ×, /).

  • generator_numer : ℕ The generating element (ι_τ).

  • generator_denom : ℕ
  • gen_is_iota : self.generator_numer = Boundary.iota_tau_numer ∧ self.generator_denom = Boundary.iota_tau_denom Instances For

Tau.BookIV.Arena.instReprPhysConstCore.repr

source def Tau.BookIV.Arena.instReprPhysConstCore.repr :PhysConstCore → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.instReprPhysConstCore

source instance Tau.BookIV.Arena.instReprPhysConstCore :Repr PhysConstCore

Equations

  • Tau.BookIV.Arena.instReprPhysConstCore = { reprPrec := Tau.BookIV.Arena.instReprPhysConstCore.repr }

Tau.BookIV.Arena.phys_const_core

source def Tau.BookIV.Arena.phys_const_core :PhysConstCore

Equations

  • Tau.BookIV.Arena.phys_const_core = { generator_numer := Tau.Boundary.iota_tau_numer, generator_denom := Tau.Boundary.iota_tau_denom, gen_is_iota := Tau.BookIV.Arena.phys_const_core._proof_1 } Instances For

Tau.BookIV.Arena.SectorLift

source structure Tau.BookIV.Arena.SectorLift :Type

[IV.D262] A canonical sector lift: Λ_S: L → τ³ projecting boundary data to a specific sector. There are 5 lifts (one per sector).

  • sector : BookIII.Sectors.Sector Target sector.

  • rational : Bool The lift produces rational functions of ι_τ.

  • rational_true : self.rational = true Instances For

Tau.BookIV.Arena.instReprSectorLift.repr

source def Tau.BookIV.Arena.instReprSectorLift.repr :SectorLift → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.instReprSectorLift

source instance Tau.BookIV.Arena.instReprSectorLift :Repr SectorLift

Equations

  • Tau.BookIV.Arena.instReprSectorLift = { reprPrec := Tau.BookIV.Arena.instReprSectorLift.repr }

Tau.BookIV.Arena.all_sector_lifts

source def Tau.BookIV.Arena.all_sector_lifts :List SectorLift

All 5 canonical sector lifts. Equations

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

Tau.BookIV.Arena.BoundaryChartReadout

source structure Tau.BookIV.Arena.BoundaryChartReadout :Type

[IV.D263] Chart readout from boundary data: assembles sector lifts into a coherent 4D readout.

  • lift_count : ℕ Number of sector lifts used.

  • lift_count_eq : self.lift_count = 5

  • output_dim : ℕ Output dimension.

  • output_eq : self.output_dim = 4 Instances For

Tau.BookIV.Arena.instReprBoundaryChartReadout

source instance Tau.BookIV.Arena.instReprBoundaryChartReadout :Repr BoundaryChartReadout

Equations

  • Tau.BookIV.Arena.instReprBoundaryChartReadout = { reprPrec := Tau.BookIV.Arena.instReprBoundaryChartReadout.repr }

Tau.BookIV.Arena.instReprBoundaryChartReadout.repr

source def Tau.BookIV.Arena.instReprBoundaryChartReadout.repr :BoundaryChartReadout → ℕ → Std.Format

Equations

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

Tau.BookIV.Arena.smooth_from_coherent

source theorem Tau.BookIV.Arena.smooth_from_coherent :all_sector_lifts.length = 5 ∧ chart_readout.target_dim = 4

[IV.P153] Coherent chart readouts produce smooth manifold structure. When sector lifts are mutually consistent, the readout space is a smooth 4-manifold (locally ℝ⁴).

Tau.BookIV.Arena.boundary_triad

source theorem Tau.BookIV.Arena.boundary_triad :1 + 1 + 1 = 3 ∧ CharacterType.ChiPlus ≠ CharacterType.ChiMinus ∧ all_sector_lifts.length = 5 ∧ chart_readout.target_dim = 4

[IV.T97] Boundary Triad Theorem: the boundary L carries exactly 3 canonical structures: (1) bipolar characters, (2) sector lifts, (3) chart readouts. These are the complete set of observable data.