TauLib · API Book II

TauLib.BookII.Interior.TauAdmissible

TauLib.BookII.Interior.TauAdmissible

τ-admissible points: the coordinate space of τ³.

Registry Cross-References

  • [II.D02] τ-Admissible Point — TauAdmissiblePoint, from_tau_idx

  • [II.D03] Constraint Lattice — constraint_C1 .. constraint_C5

  • [II.T01] Point Set Well-Defined — round_trip_check, admissible_check

Mathematical Content

A τ-admissible point is a quadruple (A, B, C, D) ∈ τ-Idx⁴ satisfying:

  • C1: A ∈ ℙ_τ ∪ {1} (prime or unity)

  • C2: B, C, D ≥ 0 (non-negativity; automatic for ℕ)

  • C3: every prime factor of D is strictly < A

  • C4: if A = 1 then B = 0 and C = 0

  • C5: normalization (greedy peel consistency)

The point set τ³ := τ³_fin ∪ τ³_lim is well-defined:

  • τ³_fin bijects with Obj(τ) via the ABCD chart Φ

  • τ³_lim is non-empty (primorial tower)

  • τ³ is closed under CRT reduction

Tau.BookII.Interior.constraint_C1

source def Tau.BookII.Interior.constraint_C1 (a : Denotation.TauIdx) :Bool

[II.D03/C1] Prime constraint: A is prime or 1. Equations

  • Tau.BookII.Interior.constraint_C1 a = (Tau.Coordinates.is_prime_bool a || a == 1) Instances For

Tau.BookII.Interior.largest_prime_factor_aux

source@[irreducible]

def Tau.BookII.Interior.largest_prime_factor_aux (n d best fuel : Nat) :Nat

[II.D03/C3] Remainder constraint: largest prime factor of D < A. Returns true if all prime factors of d are strictly less than bound. Equations

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

Tau.BookII.Interior.largest_prime_factor

source def Tau.BookII.Interior.largest_prime_factor (n : Denotation.TauIdx) :Denotation.TauIdx

Largest prime factor of n, or 0 if n ≤ 1. Equations

  • Tau.BookII.Interior.largest_prime_factor n = if n ≤ 1 then 0 else Tau.BookII.Interior.largest_prime_factor_aux n 2 0 n Instances For

Tau.BookII.Interior.constraint_C3

source def Tau.BookII.Interior.constraint_C3 (d a : Denotation.TauIdx) :Bool

[II.D03/C3] Every prime factor of D is strictly < A. Equations

  • Tau.BookII.Interior.constraint_C3 d a = (decide (d ≤ 1) || decide (Tau.BookII.Interior.largest_prime_factor d < a)) Instances For

Tau.BookII.Interior.constraint_C4

source def Tau.BookII.Interior.constraint_C4 (a b c : Denotation.TauIdx) :Bool

[II.D03/C4] Tower constraint: if A = 1 then B = C = 0. Equations

  • Tau.BookII.Interior.constraint_C4 a b c = if (a == 1) = true then b == 0 && c == 0 else true Instances For

Tau.BookII.Interior.constraint_C5

source def Tau.BookII.Interior.constraint_C5 (a b c d : Denotation.TauIdx) :Bool

[II.D03/C5] Normalization: round-trip through abcd_chart is consistent. Equations

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

Tau.BookII.Interior.is_tau_admissible

source def Tau.BookII.Interior.is_tau_admissible (a b c d : Denotation.TauIdx) :Bool

[II.D03] Full constraint lattice check for a candidate (A, B, C, D). Equations

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

Tau.BookII.Interior.TauAdmissiblePoint

source structure Tau.BookII.Interior.TauAdmissiblePoint :Type

[II.D02] A τ-admissible point: ABCD quadruple from the greedy peel decomposition. Every object X ∈ Obj(τ) has a unique such representation via the Hyperfactorization Theorem (I.T04).

  • a : Denotation.TauIdx
  • b : Denotation.TauIdx
  • c : Denotation.TauIdx
  • d : Denotation.TauIdx Instances For

Tau.BookII.Interior.instReprTauAdmissiblePoint

source instance Tau.BookII.Interior.instReprTauAdmissiblePoint :Repr TauAdmissiblePoint

Equations

  • Tau.BookII.Interior.instReprTauAdmissiblePoint = { reprPrec := Tau.BookII.Interior.instReprTauAdmissiblePoint.repr }

Tau.BookII.Interior.instReprTauAdmissiblePoint.repr

source def Tau.BookII.Interior.instReprTauAdmissiblePoint.repr :TauAdmissiblePoint → Nat → Std.Format

Equations

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

Tau.BookII.Interior.instDecidableEqTauAdmissiblePoint.decEq

source def Tau.BookII.Interior.instDecidableEqTauAdmissiblePoint.decEq (x✝ x✝¹ : TauAdmissiblePoint) :Decidable (x✝ = x✝¹)

Equations

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

Tau.BookII.Interior.instDecidableEqTauAdmissiblePoint

source instance Tau.BookII.Interior.instDecidableEqTauAdmissiblePoint :DecidableEq TauAdmissiblePoint

Equations

  • Tau.BookII.Interior.instDecidableEqTauAdmissiblePoint = Tau.BookII.Interior.instDecidableEqTauAdmissiblePoint.decEq

Tau.BookII.Interior.from_tau_idx

source def Tau.BookII.Interior.from_tau_idx (x : Denotation.TauIdx) :TauAdmissiblePoint

Construct τ-admissible point from a τ-index via the ABCD chart. Equations

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

Tau.BookII.Interior.to_tau_idx

source def Tau.BookII.Interior.to_tau_idx (p : TauAdmissiblePoint) :Denotation.TauIdx

Reconstruct τ-index from an admissible point: T(A,B,C) · D. Equations

  • Tau.BookII.Interior.to_tau_idx p = Tau.Coordinates.tower_atom p.a p.b p.c * p.d Instances For

Tau.BookII.Interior.TauAdmissiblePoint.valid

source def Tau.BookII.Interior.TauAdmissiblePoint.valid (p : TauAdmissiblePoint) :Bool

Check that a TauAdmissiblePoint satisfies all constraints. Equations

  • p.valid = Tau.BookII.Interior.is_tau_admissible p.a p.b p.c p.d Instances For

Tau.BookII.Interior.round_trip_check

source def Tau.BookII.Interior.round_trip_check (x : Denotation.TauIdx) :Bool

[II.T01, clause 1] Round-trip: from_tau_idx ∘ to_tau_idx is consistent with chart_value. Equations

  • Tau.BookII.Interior.round_trip_check x = (Tau.BookII.Interior.to_tau_idx (Tau.BookII.Interior.from_tau_idx x) == x) Instances For

Tau.BookII.Interior.admissible_check

source def Tau.BookII.Interior.admissible_check (x : Denotation.TauIdx) :Bool

[II.T01, clause 1] Admissibility: ABCD chart always produces admissible quadruples. Equations

  • Tau.BookII.Interior.admissible_check x = (Tau.BookII.Interior.from_tau_idx x).valid Instances For

Tau.BookII.Interior.batch_verify

source def Tau.BookII.Interior.batch_verify (bound : Denotation.TauIdx) :Bool

[II.T01, clause 1] Batch verification for X = 2..bound. Equations

  • Tau.BookII.Interior.batch_verify bound = Tau.BookII.Interior.batch_verify.go bound 2 (bound + 1) Instances For

Tau.BookII.Interior.batch_verify.go

source@[irreducible]

**def Tau.BookII.Interior.batch_verify.go (bound : Denotation.TauIdx)

(start fuel : Nat) :Bool**

Equations

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

Tau.BookII.Interior.primorial_witness

source def Tau.BookII.Interior.primorial_witness :List (Denotation.TauIdx × TauAdmissiblePoint)

Primorial P_k = p₁ · p₂ · … · p_k. Equations

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

Tau.BookII.Interior.primorial_b_eq_one

source def Tau.BookII.Interior.primorial_b_eq_one :Bool

Primorial readouts have A = p_k, B = 1, C = 1, D = P_{k-1}. Equations

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

Tau.BookII.Interior.primorial_c_eq_one

source def Tau.BookII.Interior.primorial_c_eq_one :Bool

Equations

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

Tau.BookII.Interior.primorial_a_increasing

source def Tau.BookII.Interior.primorial_a_increasing :Bool

Primorial A-values form an increasing sequence of primes. Equations

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

Tau.BookII.Interior.admissible_2_to_20

source theorem Tau.BookII.Interior.admissible_2_to_20 :batch_verify 20 = true