TauLib · API Book II

TauLib.BookII.Closure.GeometricBiSquare

TauLib.BookII.Closure.GeometricBiSquare

The Geometric Bi-Square: Book I’s algebraic bi-square (I.T41) filled with the geometric objects earned in Book II Parts I-IX.

Registry Cross-References

  • [II.D77] Geometric Bi-Square – GeometricBiSquareData, compute_geometric_bisquare

  • [II.T49] Geometric Bi-Square Theorem – geometric_bisquare_check

  • [II.R33] Algebraic-to-Geometric Audit – algebraic_geometric_audit

  • [II.R34] Scaling Chain Forward – ScalingLevel, scaling_chain_check

Mathematical Content

The algebraic bi-square (I.T41) is a pasted commuting diagram on finite cyclic groups Z/M_kZ:

  • Left square: tower coherence (reduce(f_l(n), k) = f_k(n))

  • Right square: spectral naturality (chi_+/chi_- decomposition)

  • Limit principle: agreement at one depth implies agreement below

Book II fills this algebraic skeleton with geometric content:

  • Domain L becomes S^1 v S^1 via torus degeneration (II.T13)

  • Interior tau^3 becomes Stone space (II.T07)

  • Codomain becomes calibrated H_tau (II.D35)

  • Spectral algebra becomes A_spec(L) (II.D60)

  • Limit principle becomes Central Theorem (II.T40)

The Geometric Bi-Square Theorem (II.T49) asserts all eight components are earned, all commuting squares are continuous, and the limit row is precisely the Central Theorem.

Tau.BookII.Closure.GeometricBiSquareData

source structure Tau.BookII.Closure.GeometricBiSquareData :Type

[II.D77] The Geometric Bi-Square: Book I’s algebraic bi-square (I.T41) annotated with boolean witnesses recording that each geometric component has been earned in Book II.

Eight witnesses correspond to eight geometric “earnings”:

  • topology_earned: Stone space structure on tau^3 (II.T07)

  • continuity_earned: Hol implies Continuous (II.T06)

  • geometry_earned: Tarski axioms verified (II.T16-T20)

  • torus_degeneration_earned: T^2 -> S^1 v S^1 (II.T13)

  • calibration_earned: H_tau calibrated with pi, e, j (II.D35)

  • spectral_algebra_earned: A_spec(L) ring structure (II.D60)

  • central_theorem_earned: O(tau^3) = A_spec(L) (II.T40)

  • hartogs_earned: Mutual determination (II.T27)

  • topology_earned : Bool Stone space structure on tau^3 (II.T07).

  • continuity_earned : Bool Hol implies Continuous (II.T06).

  • geometry_earned : Bool Tarski axioms verified (II.T16-T20).

  • torus_degeneration_earned : Bool T^2 -> S^1 v S^1 via pinch map (II.T13).

  • calibration_earned : Bool H_tau calibrated with pi, e, j (II.D35).

  • spectral_algebra_earned : Bool A_spec(L) ring/tower structure (II.D60).

  • central_theorem_earned : Bool Central Theorem O(tau^3) = A_spec(L) (II.T40).

  • hartogs_earned : Bool Mutual determination / Hartogs (II.T27).

Instances For

Tau.BookII.Closure.instReprGeometricBiSquareData.repr

source def Tau.BookII.Closure.instReprGeometricBiSquareData.repr :GeometricBiSquareData → ℕ → Std.Format

Equations

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

Tau.BookII.Closure.instReprGeometricBiSquareData

source instance Tau.BookII.Closure.instReprGeometricBiSquareData :Repr GeometricBiSquareData

Equations

  • Tau.BookII.Closure.instReprGeometricBiSquareData = { reprPrec := Tau.BookII.Closure.instReprGeometricBiSquareData.repr }

Tau.BookII.Closure.instDecidableEqGeometricBiSquareData.decEq

source def Tau.BookII.Closure.instDecidableEqGeometricBiSquareData.decEq (x✝ x✝¹ : GeometricBiSquareData) :Decidable (x✝ = x✝¹)

Equations

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

Tau.BookII.Closure.instDecidableEqGeometricBiSquareData

source instance Tau.BookII.Closure.instDecidableEqGeometricBiSquareData :DecidableEq GeometricBiSquareData

Equations

  • Tau.BookII.Closure.instDecidableEqGeometricBiSquareData = Tau.BookII.Closure.instDecidableEqGeometricBiSquareData.decEq

Tau.BookII.Closure.compute_geometric_bisquare

source def Tau.BookII.Closure.compute_geometric_bisquare (db bound : Denotation.TauIdx) :GeometricBiSquareData

[II.D77] Compute the Geometric Bi-Square by evaluating all eight geometric check functions from Book II. Parameters db, bound control verification depth. Equations

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

Tau.BookII.Closure.geometric_bisquare_complete

source def Tau.BookII.Closure.geometric_bisquare_complete (gbs : GeometricBiSquareData) :Bool

[II.D77] Check that all eight components are earned. Equations

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

Tau.BookII.Closure.geometric_bisquare_check

source def Tau.BookII.Closure.geometric_bisquare_check (db bound : Denotation.TauIdx) :Bool

[II.T49] The Geometric Bi-Square Theorem: compute and verify that all eight geometric components are earned. Equations

  • Tau.BookII.Closure.geometric_bisquare_check db bound = Tau.BookII.Closure.geometric_bisquare_complete (Tau.BookII.Closure.compute_geometric_bisquare db bound) Instances For

Tau.BookII.Closure.geometric_component_count

source def Tau.BookII.Closure.geometric_component_count (gbs : GeometricBiSquareData) :ℕ

[II.T49] Count how many geometric components are verified (out of 8). Equations

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

Tau.BookII.Closure.algebraic_geometric_audit

source def Tau.BookII.Closure.algebraic_geometric_audit (db bound k_max : Denotation.TauIdx) :Bool

[II.R33] Algebraic-to-Geometric Audit: record which Book I algebraic components have received geometric content in Book II. The audit passes when all eight components are earned AND the E1 export package is complete. Equations

  • Tau.BookII.Closure.algebraic_geometric_audit db bound k_max = (Tau.BookII.Closure.geometric_bisquare_check db bound && Tau.BookII.Closure.full_export_check db bound k_max) Instances For

Tau.BookII.Closure.algebraic_core

source def Tau.BookII.Closure.algebraic_core :Holomorphy.BookICrownJewel

The algebraic core: the Book I crown jewel is always available regardless of the geometric witnesses. This is a definitional identity: the algebraic bi-square (I.T41) exists independently of whether Book II’s geometry is earned. Equations

  • Tau.BookII.Closure.algebraic_core = Tau.Holomorphy.book_i_crown_jewel Instances For

Tau.BookII.Closure.compatibility_with_algebraic

source theorem Tau.BookII.Closure.compatibility_with_algebraic (f : Holomorphy.StageFun) :Holomorphy.TowerCoherent f ↔ (∀ (n k l : Denotation.TauIdx), k ≤ l → Polarity.reduce (f.b_fun n l) k = f.b_fun n k) ∧ ∀ (n k l : Denotation.TauIdx), k ≤ l → Polarity.reduce (f.c_fun n l) k = f.c_fun n k

Compatibility: the algebraic bi-square characterization is preserved. Forgetting geometry recovers I.T41.

Tau.BookII.Closure.geometric_preserves_limit

source **theorem Tau.BookII.Closure.geometric_preserves_limit (f₁ f₂ : Holomorphy.StageFun)

(h₁ : Holomorphy.TowerCoherent f₁)

(h₂ : Holomorphy.TowerCoherent f₂)

(d₀ : Denotation.TauIdx)

(h : ∀ (n : Denotation.TauIdx), Holomorphy.agree_at f₁ f₂ n d₀)

(n k : Denotation.TauIdx) :k ≤ d₀ → Holomorphy.agree_at f₁ f₂ n k**

Compatibility: the limit principle survives geometrization.

Tau.BookII.Closure.geometric_preserves_right_auto

source **theorem Tau.BookII.Closure.geometric_preserves_right_auto (f : Holomorphy.StageFun)

(htc : Holomorphy.TowerCoherent f)

(n k l : Denotation.TauIdx)

(hkl : k ≤ l) :Holomorphy.spectral_of f n k = { b_coeff := Polarity.reduce (Holomorphy.spectral_of f n l).b_coeff k, c_coeff := Polarity.reduce (Holomorphy.spectral_of f n l).c_coeff k }**

Compatibility: right-square automaticity survives geometrization.

Tau.BookII.Closure.ScalingLevel

source inductive Tau.BookII.Closure.ScalingLevel :Type

[II.R34] The three enrichment levels at which the bi-square lives.

  • E0_algebraic: Book I (finite cyclic groups, no topology)

  • E1_geometric: Book II (Stone space, continuity, torus degeneration)

  • E2_enriched: Book III (spectral forces, preview only)

  • E0_algebraic : ScalingLevel
  • E1_geometric : ScalingLevel
  • E2_enriched : ScalingLevel Instances For

Tau.BookII.Closure.instReprScalingLevel

source instance Tau.BookII.Closure.instReprScalingLevel :Repr ScalingLevel

Equations

  • Tau.BookII.Closure.instReprScalingLevel = { reprPrec := Tau.BookII.Closure.instReprScalingLevel.repr }

Tau.BookII.Closure.instReprScalingLevel.repr

source def Tau.BookII.Closure.instReprScalingLevel.repr :ScalingLevel → ℕ → Std.Format

Equations

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

Tau.BookII.Closure.instDecidableEqScalingLevel

source instance Tau.BookII.Closure.instDecidableEqScalingLevel :DecidableEq ScalingLevel

Equations

  • Tau.BookII.Closure.instDecidableEqScalingLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Tau.BookII.Closure.scaling_level_index

source def Tau.BookII.Closure.scaling_level_index :ScalingLevel → ℕ

[II.R34] The scaling chain: algebraic < geometric < enriched. Each level adds geometric content to the bi-square. Equations

  • Tau.BookII.Closure.scaling_level_index Tau.BookII.Closure.ScalingLevel.E0_algebraic = 0
  • Tau.BookII.Closure.scaling_level_index Tau.BookII.Closure.ScalingLevel.E1_geometric = 1
  • Tau.BookII.Closure.scaling_level_index Tau.BookII.Closure.ScalingLevel.E2_enriched = 2 Instances For

Tau.BookII.Closure.scaling_chain_check

source def Tau.BookII.Closure.scaling_chain_check :Bool

[II.R34] Scaling chain monotonicity: E0 < E1 < E2. Equations

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

Tau.BookII.Closure.book2_scaling_level

source def Tau.BookII.Closure.book2_scaling_level :ScalingLevel

[II.R34] Book II lives at E1_geometric. Equations

  • Tau.BookII.Closure.book2_scaling_level = Tau.BookII.Closure.ScalingLevel.E1_geometric Instances For

Tau.BookII.Closure.e2_not_yet_earned

source def Tau.BookII.Closure.e2_not_yet_earned :Bool

[II.R34] The geometric bi-square is the E1 avatar of the algebraic bi-square. The E2 avatar (enriched bi-square) will be earned in Book III. Equations

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

Tau.BookII.Closure.geometric_bisquare_3_15

source theorem Tau.BookII.Closure.geometric_bisquare_3_15 :geometric_bisquare_check 3 15 = true

Tau.BookII.Closure.geometric_all_eight

source theorem Tau.BookII.Closure.geometric_all_eight :geometric_component_count (compute_geometric_bisquare 3 15) = 8

Tau.BookII.Closure.geo_topology

source theorem Tau.BookII.Closure.geo_topology :(compute_geometric_bisquare 3 15).topology_earned = true

Tau.BookII.Closure.geo_continuity

source theorem Tau.BookII.Closure.geo_continuity :(compute_geometric_bisquare 3 15).continuity_earned = true

Tau.BookII.Closure.geo_geometry

source theorem Tau.BookII.Closure.geo_geometry :(compute_geometric_bisquare 3 15).geometry_earned = true

Tau.BookII.Closure.geo_torus_degeneration

source theorem Tau.BookII.Closure.geo_torus_degeneration :(compute_geometric_bisquare 3 15).torus_degeneration_earned = true

Tau.BookII.Closure.geo_calibration

source theorem Tau.BookII.Closure.geo_calibration :(compute_geometric_bisquare 3 15).calibration_earned = true

Tau.BookII.Closure.geo_spectral_algebra

source theorem Tau.BookII.Closure.geo_spectral_algebra :(compute_geometric_bisquare 3 15).spectral_algebra_earned = true

Tau.BookII.Closure.geo_central_theorem

source theorem Tau.BookII.Closure.geo_central_theorem :(compute_geometric_bisquare 3 15).central_theorem_earned = true

Tau.BookII.Closure.geo_hartogs

source theorem Tau.BookII.Closure.geo_hartogs :(compute_geometric_bisquare 3 15).hartogs_earned = true

Tau.BookII.Closure.audit_3_15_3

source theorem Tau.BookII.Closure.audit_3_15_3 :algebraic_geometric_audit 3 15 3 = true

Tau.BookII.Closure.scaling_chain_valid

source theorem Tau.BookII.Closure.scaling_chain_valid :scaling_chain_check = true

Tau.BookII.Closure.e2_not_earned

source theorem Tau.BookII.Closure.e2_not_earned :e2_not_yet_earned = true

Tau.BookII.Closure.complete_means_eight

source theorem Tau.BookII.Closure.complete_means_eight (gbs : GeometricBiSquareData) :geometric_bisquare_complete gbs = true → geometric_component_count gbs = 8

[II.T49] A complete geometric bi-square has all 8 components. This is the structural statement that completeness implies count = 8.

Tau.BookII.Closure.geometric_implies_central

source theorem Tau.BookII.Closure.geometric_implies_central (db bound : Denotation.TauIdx) :geometric_bisquare_check db bound = true → CentralTheorem.central_theorem_check db bound = true

[II.T49] The geometric bi-square implies the Central Theorem is earned. If the full check passes, the central_theorem_earned field is true.

Tau.BookII.Closure.e0_ne_e1

source theorem Tau.BookII.Closure.e0_ne_e1 :ScalingLevel.E0_algebraic ≠ ScalingLevel.E1_geometric

[II.R34] E0 and E1 are distinct scaling levels.

Tau.BookII.Closure.e1_ne_e2

source theorem Tau.BookII.Closure.e1_ne_e2 :ScalingLevel.E1_geometric ≠ ScalingLevel.E2_enriched

[II.R34] E1 and E2 are distinct scaling levels.