TauLib · API Book III

TauLib.BookIII.Bridge.TranslationObstruction

TauLib.BookIII.Bridge.TranslationObstruction

Translation obstruction theory: where arithmetic and topological translations fail, characterized by forbidden moves.

Registry Cross-References

  • [III.D91] Obstruction Cocycle — obstruction_value, obstruction_check

  • [III.D92] Forbidden Move Obstruction Classes — move_obstructs_arith, move_obstructs_topo

  • [III.T61] Translation Failure Boundary — translation_failure_boundary_check

  • [III.P38] P vs NP as Polynomial Translation Obstruction — pvsnp_obstruction_check

Mathematical Content

III.D91 (Obstruction Cocycle): For each forbidden move fm, the obstruction value measures how much the translation deviates from faithfulness. For mild moves (damage 1), the deviation is bounded. For breaking moves (damage 3), the deviation grows with primorial depth.

III.D92 (Forbidden Move Obstruction Classes): Each of the 5 forbidden moves obstructs either the arithmetic or topological translation in a specific way:

  • unbounded_fanout: blocks arithmetic (CRT decomposition unbounded)

  • global_equality: blocks topological (NF not unique globally)

  • succinct_circuits: blocks both (P vs NP)

  • exponential_quantification: blocks both (requires E₃)

  • nonlocal_disguise: blocks topological (multiple representations)

III.T61 (Translation Failure Boundary): The translations Arith_tr and Topo_tr are faithful EXACTLY on the complement of the 5 forbidden moves. The failure boundary is sharp: the translation works perfectly within the safe region and degenerates precisely at forbidden operations.

III.P38 (P vs NP Obstruction): P vs NP is the statement that polynomial-time translation of NP-complete problems is impossible. In τ-terms: the succinct_circuits forbidden move has damage 3 (bridge breaks), meaning P_adm = NP_adm in τ (internal equivalence) but this cannot be translated to ZFC as P = NP or P ≠ NP (independence).

Tau.BookIII.Bridge.TranslationObstruction

source inductive Tau.BookIII.Bridge.TranslationObstruction :Type

Forbidden move type (mirrors ForbiddenMoves.lean).

  • unbounded_fanout : TranslationObstruction
  • global_equality : TranslationObstruction
  • succinct_circuits : TranslationObstruction
  • exponential_quantification : TranslationObstruction
  • nonlocal_disguise : TranslationObstruction Instances For

Tau.BookIII.Bridge.instReprTranslationObstruction.repr

source def Tau.BookIII.Bridge.instReprTranslationObstruction.repr :TranslationObstruction → ℕ → Std.Format

Equations

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

Tau.BookIII.Bridge.instReprTranslationObstruction

source instance Tau.BookIII.Bridge.instReprTranslationObstruction :Repr TranslationObstruction

Equations

  • Tau.BookIII.Bridge.instReprTranslationObstruction = { reprPrec := Tau.BookIII.Bridge.instReprTranslationObstruction.repr }

Tau.BookIII.Bridge.instDecidableEqTranslationObstruction

source instance Tau.BookIII.Bridge.instDecidableEqTranslationObstruction :DecidableEq TranslationObstruction

Equations

  • Tau.BookIII.Bridge.instDecidableEqTranslationObstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Tau.BookIII.Bridge.instBEqTranslationObstruction

source instance Tau.BookIII.Bridge.instBEqTranslationObstruction :BEq TranslationObstruction

Equations

  • Tau.BookIII.Bridge.instBEqTranslationObstruction = { beq := Tau.BookIII.Bridge.instBEqTranslationObstruction.beq }

Tau.BookIII.Bridge.instBEqTranslationObstruction.beq

source def Tau.BookIII.Bridge.instBEqTranslationObstruction.beq :TranslationObstruction → TranslationObstruction → Bool

Equations

  • Tau.BookIII.Bridge.instBEqTranslationObstruction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx) Instances For

Tau.BookIII.Bridge.obstruction_damage

source def Tau.BookIII.Bridge.obstruction_damage (obs : TranslationObstruction) :ℕ

Bridge damage level for each obstruction. Equations

  • Tau.BookIII.Bridge.obstruction_damage Tau.BookIII.Bridge.TranslationObstruction.unbounded_fanout = 2
  • Tau.BookIII.Bridge.obstruction_damage Tau.BookIII.Bridge.TranslationObstruction.global_equality = 1
  • Tau.BookIII.Bridge.obstruction_damage Tau.BookIII.Bridge.TranslationObstruction.succinct_circuits = 3
  • Tau.BookIII.Bridge.obstruction_damage Tau.BookIII.Bridge.TranslationObstruction.exponential_quantification = 3
  • Tau.BookIII.Bridge.obstruction_damage Tau.BookIII.Bridge.TranslationObstruction.nonlocal_disguise = 1 Instances For

Tau.BookIII.Bridge.obstruction_value

source **def Tau.BookIII.Bridge.obstruction_value (obs : TranslationObstruction)

(k : ℕ) :ℕ**

[III.D91] Obstruction value at stage k: measures deviation from faithful translation. Higher = worse. Equations

  • Tau.BookIII.Bridge.obstruction_value Tau.BookIII.Bridge.TranslationObstruction.unbounded_fanout k = k
  • Tau.BookIII.Bridge.obstruction_value Tau.BookIII.Bridge.TranslationObstruction.global_equality k = 0
  • Tau.BookIII.Bridge.obstruction_value Tau.BookIII.Bridge.TranslationObstruction.succinct_circuits k = if Tau.Polarity.primorial k > 0 then Tau.Polarity.primorial k else 0
  • Tau.BookIII.Bridge.obstruction_value Tau.BookIII.Bridge.TranslationObstruction.exponential_quantification k = if Tau.Polarity.primorial k > 0 then Tau.Polarity.primorial k else 0
  • Tau.BookIII.Bridge.obstruction_value Tau.BookIII.Bridge.TranslationObstruction.nonlocal_disguise k = 0 Instances For

Tau.BookIII.Bridge.obstruction_check

source def Tau.BookIII.Bridge.obstruction_check (db : ℕ) :Bool

[III.D91] Obstruction check: verify obstruction values match expected damage levels. Equations

  • Tau.BookIII.Bridge.obstruction_check db = Tau.BookIII.Bridge.obstruction_check.go db 1 (db + 1) Instances For

Tau.BookIII.Bridge.obstruction_check.go

source@[irreducible]

def Tau.BookIII.Bridge.obstruction_check.go (db k fuel : ℕ) :Bool

Equations

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

Tau.BookIII.Bridge.move_obstructs_arith

source def Tau.BookIII.Bridge.move_obstructs_arith (obs : TranslationObstruction) :Bool

[III.D92] Does this move obstruct arithmetic translation? Equations

  • Tau.BookIII.Bridge.move_obstructs_arith Tau.BookIII.Bridge.TranslationObstruction.unbounded_fanout = true
  • Tau.BookIII.Bridge.move_obstructs_arith Tau.BookIII.Bridge.TranslationObstruction.global_equality = false
  • Tau.BookIII.Bridge.move_obstructs_arith Tau.BookIII.Bridge.TranslationObstruction.succinct_circuits = true
  • Tau.BookIII.Bridge.move_obstructs_arith Tau.BookIII.Bridge.TranslationObstruction.exponential_quantification = true
  • Tau.BookIII.Bridge.move_obstructs_arith Tau.BookIII.Bridge.TranslationObstruction.nonlocal_disguise = false Instances For

Tau.BookIII.Bridge.move_obstructs_topo

source def Tau.BookIII.Bridge.move_obstructs_topo (obs : TranslationObstruction) :Bool

[III.D92] Does this move obstruct topological translation? Equations

  • Tau.BookIII.Bridge.move_obstructs_topo Tau.BookIII.Bridge.TranslationObstruction.unbounded_fanout = false
  • Tau.BookIII.Bridge.move_obstructs_topo Tau.BookIII.Bridge.TranslationObstruction.global_equality = true
  • Tau.BookIII.Bridge.move_obstructs_topo Tau.BookIII.Bridge.TranslationObstruction.succinct_circuits = true
  • Tau.BookIII.Bridge.move_obstructs_topo Tau.BookIII.Bridge.TranslationObstruction.exponential_quantification = true
  • Tau.BookIII.Bridge.move_obstructs_topo Tau.BookIII.Bridge.TranslationObstruction.nonlocal_disguise = true Instances For

Tau.BookIII.Bridge.arith_obstruction_count

source def Tau.BookIII.Bridge.arith_obstruction_count :ℕ

[III.D92] Count how many obstructions affect arithmetic. Equations

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

Tau.BookIII.Bridge.topo_obstruction_count

source def Tau.BookIII.Bridge.topo_obstruction_count :ℕ

[III.D92] Count how many obstructions affect topology. Equations

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

Tau.BookIII.Bridge.safe_region_check

source def Tau.BookIII.Bridge.safe_region_check (bound db : ℕ) :Bool

[III.T61] Safe region check: within the safe region (no forbidden moves invoked), both translations are perfectly faithful. Equations

  • Tau.BookIII.Bridge.safe_region_check bound db = Tau.BookIII.Bridge.safe_region_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Bridge.safe_region_check.go

source@[irreducible]

def Tau.BookIII.Bridge.safe_region_check.go (bound db x k fuel : ℕ) :Bool

Equations

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

Tau.BookIII.Bridge.translation_failure_boundary_check

source def Tau.BookIII.Bridge.translation_failure_boundary_check (bound db : ℕ) :Bool

[III.T61] Full translation failure boundary. Equations

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

Tau.BookIII.Bridge.pvsnp_obstruction_check

source def Tau.BookIII.Bridge.pvsnp_obstruction_check (db : ℕ) :Bool

[III.P38] P vs NP obstruction: the succinct_circuits move has damage 3, meaning the bridge breaks entirely. At each finite stage k, P_adm = NP_adm (all problems decidable in finite Z/M_k Z), but this internal equivalence cannot be translated. Equations

  • Tau.BookIII.Bridge.pvsnp_obstruction_check db = Tau.BookIII.Bridge.pvsnp_obstruction_check.go db 1 (db + 1) Instances For

Tau.BookIII.Bridge.pvsnp_obstruction_check.go

source@[irreducible]

def Tau.BookIII.Bridge.pvsnp_obstruction_check.go (db k fuel : ℕ) :Bool

Equations

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

Tau.BookIII.Bridge.pvsnp_obstruction_check.log_approx

source def Tau.BookIII.Bridge.pvsnp_obstruction_check.log_approx (n : ℕ) :ℕ

Equations

  • Tau.BookIII.Bridge.pvsnp_obstruction_check.log_approx n = Tau.BookIII.Bridge.pvsnp_obstruction_check.go_log n 0 Instances For

Tau.BookIII.Bridge.pvsnp_obstruction_check.go_log

source@[irreducible]

def Tau.BookIII.Bridge.pvsnp_obstruction_check.go_log (n acc : ℕ) :ℕ

Equations

  • Tau.BookIII.Bridge.pvsnp_obstruction_check.go_log n acc = if n ≤ 1 then acc else Tau.BookIII.Bridge.pvsnp_obstruction_check.go_log (n / 2) (acc + 1) Instances For

Tau.BookIII.Bridge.obstruction_check_3

source theorem Tau.BookIII.Bridge.obstruction_check_3 :obstruction_check 3 = true

[III.D91] Obstruction values correct at depth 3.

Tau.BookIII.Bridge.arith_obstruction_3

source theorem Tau.BookIII.Bridge.arith_obstruction_3 :arith_obstruction_count = 3

[III.D92] Arithmetic has 3 obstruction classes.

Tau.BookIII.Bridge.topo_obstruction_4

source theorem Tau.BookIII.Bridge.topo_obstruction_4 :topo_obstruction_count = 4

[III.D92] Topology has 4 obstruction classes.

Tau.BookIII.Bridge.safe_region_8_3

source theorem Tau.BookIII.Bridge.safe_region_8_3 :safe_region_check 8 3 = true

[III.T61] Safe region faithful at bound 8, depth 3.

Tau.BookIII.Bridge.translation_boundary_8_3

source theorem Tau.BookIII.Bridge.translation_boundary_8_3 :translation_failure_boundary_check 8 3 = true

[III.T61] Translation failure boundary at bound 8, depth 3.

Tau.BookIII.Bridge.pvsnp_obstruction_3

source theorem Tau.BookIII.Bridge.pvsnp_obstruction_3 :pvsnp_obstruction_check 3 = true

[III.P38] P vs NP obstruction at depth 3.