TauLib · API Book VI

TauLib.BookVI.Sectors.Absence

TauLib.BookVI.Sectors.Absence

Failure modes: NoDist and NoSelfDesc. Virus, neutron, NS counterexamples.

Registry Cross-References

  • [VI.D21] NoDist — NoDist

  • [VI.D22] NoSelfDesc — NoSelfDesc

  • [VI.T15] Virus NoDist — virus_nodist

  • [VI.L06] NS-NoSelfDesc — ns_noselfdesc

  • [VI.L07] Consumer Bridge to E₃ — consumer_bridge_e3

  • [VI.P09] Circadian 24h = τ¹ Rotation — circadian_rotation

Ground Truth Sources

  • Book VI Chapter 10 (2nd Edition): Predictions by Absence

Tau.BookVI.Absence.NoDist

source structure Tau.BookVI.Absence.NoDist :Type

[VI.D21] NoDist: system fails τ-Distinction.

  • conditions_failed : ℕ
  • at_least_one : self.conditions_failed ≥ 1 Instances For

Tau.BookVI.Absence.instReprNoDist.repr

source def Tau.BookVI.Absence.instReprNoDist.repr :NoDist → ℕ → Std.Format

Equations

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

Tau.BookVI.Absence.instReprNoDist

source instance Tau.BookVI.Absence.instReprNoDist :Repr NoDist

Equations

  • Tau.BookVI.Absence.instReprNoDist = { reprPrec := Tau.BookVI.Absence.instReprNoDist.repr }

Tau.BookVI.Absence.NoSelfDesc

source structure Tau.BookVI.Absence.NoSelfDesc :Type

[VI.D22] NoSelfDesc: has Distinction but fails SelfDesc.

  • has_distinction : Bool
  • selfdesc_fails : Bool
  • failure_reason : String Instances For

Tau.BookVI.Absence.instReprNoSelfDesc

source instance Tau.BookVI.Absence.instReprNoSelfDesc :Repr NoSelfDesc

Equations

  • Tau.BookVI.Absence.instReprNoSelfDesc = { reprPrec := Tau.BookVI.Absence.instReprNoSelfDesc.repr }

Tau.BookVI.Absence.instReprNoSelfDesc.repr

source def Tau.BookVI.Absence.instReprNoSelfDesc.repr :NoSelfDesc → ℕ → Std.Format

Equations

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

Tau.BookVI.Absence.VirusNoDist

source structure Tau.BookVI.Absence.VirusNoDist :Type

[VI.T15] Virus NoDist: fails 3/5 distinction conditions outside host.

  • conditions_failed : ℕ
  • three_fail : self.conditions_failed = 3
  • host_dependent : Bool Instances For

Tau.BookVI.Absence.instReprVirusNoDist.repr

source def Tau.BookVI.Absence.instReprVirusNoDist.repr :VirusNoDist → ℕ → Std.Format

Equations

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

Tau.BookVI.Absence.instReprVirusNoDist

source instance Tau.BookVI.Absence.instReprVirusNoDist :Repr VirusNoDist

Equations

  • Tau.BookVI.Absence.instReprVirusNoDist = { reprPrec := Tau.BookVI.Absence.instReprVirusNoDist.repr }

Tau.BookVI.Absence.virus

source def Tau.BookVI.Absence.virus :VirusNoDist

Equations

  • Tau.BookVI.Absence.virus = { conditions_failed := 3, three_fail := Tau.BookVI.Absence.virus._proof_1 } Instances For

Tau.BookVI.Absence.virus_nodist

source theorem Tau.BookVI.Absence.virus_nodist :virus.conditions_failed = 3 ∧ virus.host_dependent = true

Tau.BookVI.Absence.NSNoSelfDesc

source structure Tau.BookVI.Absence.NSNoSelfDesc :Type

[VI.L06] NS-NoSelfDesc: 5/5 distinction, fails SelfDesc.

  • distinction_passed : ℕ
  • all_five : self.distinction_passed = 5
  • selfdesc_fails : Bool Instances For

Tau.BookVI.Absence.instReprNSNoSelfDesc.repr

source def Tau.BookVI.Absence.instReprNSNoSelfDesc.repr :NSNoSelfDesc → ℕ → Std.Format

Equations

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

Tau.BookVI.Absence.instReprNSNoSelfDesc

source instance Tau.BookVI.Absence.instReprNSNoSelfDesc :Repr NSNoSelfDesc

Equations

  • Tau.BookVI.Absence.instReprNSNoSelfDesc = { reprPrec := Tau.BookVI.Absence.instReprNSNoSelfDesc.repr }

Tau.BookVI.Absence.ns_nosd

source def Tau.BookVI.Absence.ns_nosd :NSNoSelfDesc

Equations

  • Tau.BookVI.Absence.ns_nosd = { distinction_passed := 5, all_five := Tau.BookVI.Absence.ns_nosd._proof_1 } Instances For

Tau.BookVI.Absence.ns_noselfdesc

source theorem Tau.BookVI.Absence.ns_noselfdesc :ns_nosd.distinction_passed = 5 ∧ ns_nosd.selfdesc_fails = true

Tau.BookVI.Absence.ConsumerBridgeE3

source structure Tau.BookVI.Absence.ConsumerBridgeE3 :Type

[VI.L07] Consumer sector is unique bridge-head to E₃.

  • has_eval_squared : Bool
  • consumer_only : Bool Instances For

Tau.BookVI.Absence.instReprConsumerBridgeE3

source instance Tau.BookVI.Absence.instReprConsumerBridgeE3 :Repr ConsumerBridgeE3

Equations

  • Tau.BookVI.Absence.instReprConsumerBridgeE3 = { reprPrec := Tau.BookVI.Absence.instReprConsumerBridgeE3.repr }

Tau.BookVI.Absence.instReprConsumerBridgeE3.repr

source def Tau.BookVI.Absence.instReprConsumerBridgeE3.repr :ConsumerBridgeE3 → ℕ → Std.Format

Equations

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

Tau.BookVI.Absence.consumer_bridge

source def Tau.BookVI.Absence.consumer_bridge :ConsumerBridgeE3

Equations

  • Tau.BookVI.Absence.consumer_bridge = { } Instances For

Tau.BookVI.Absence.consumer_bridge_e3

source theorem Tau.BookVI.Absence.consumer_bridge_e3 :consumer_bridge.has_eval_squared = true ∧ consumer_bridge.consumer_only = true

Tau.BookVI.Absence.CircadianRotation

source structure Tau.BookVI.Absence.CircadianRotation :Type

[VI.P09] Circadian 24h = one full α-rotation on τ¹.

  • period_hours : ℕ
  • winding_number : ℕ Instances For

Tau.BookVI.Absence.instReprCircadianRotation.repr

source def Tau.BookVI.Absence.instReprCircadianRotation.repr :CircadianRotation → ℕ → Std.Format

Equations

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

Tau.BookVI.Absence.instReprCircadianRotation

source instance Tau.BookVI.Absence.instReprCircadianRotation :Repr CircadianRotation

Equations

  • Tau.BookVI.Absence.instReprCircadianRotation = { reprPrec := Tau.BookVI.Absence.instReprCircadianRotation.repr }

Tau.BookVI.Absence.circadian

source def Tau.BookVI.Absence.circadian :CircadianRotation

Equations

  • Tau.BookVI.Absence.circadian = { } Instances For

Tau.BookVI.Absence.circadian_rotation

source theorem Tau.BookVI.Absence.circadian_rotation :circadian.period_hours = 24 ∧ circadian.winding_number = 1