TauLib · API Book VI

TauLib.BookVI.LifeCore.SelfDesc

TauLib.BookVI.LifeCore.SelfDesc

SelfDesc: the second of two Life predicates. An internal evaluator Eval_X satisfying completeness, internality, and refinement coherence.

Registry Cross-References

  • [VI.D08] SelfDesc Predicate — SelfDescPredicate

  • [VI.D09] Internal Evaluator — InternalEvaluator

  • [VI.P02] Code Reconstruction — code_reconstruction

  • [VI.T03] SelfDesc Closure Theorem — selfdesc_closure_theorem

  • [VI.P04] Seven Hallmarks Complete — seven_hallmarks_complete

Ground Truth Sources

  • Book VI Chapter 5 (2nd Edition): SelfDesc

Tau.BookVI.SelfDesc.SelfDescPredicate

source structure Tau.BookVI.SelfDesc.SelfDescPredicate :Type

[VI.D08] SelfDesc predicate: internal evaluator Eval_X satisfying completeness, internality, refinement coherence.

  • condition_count : ℕ
  • count_eq : self.condition_count = 3
  • completeness : Bool
  • internality : Bool
  • refinement_coherence : Bool Instances For

Tau.BookVI.SelfDesc.instReprSelfDescPredicate.repr

source def Tau.BookVI.SelfDesc.instReprSelfDescPredicate.repr :SelfDescPredicate → ℕ → Std.Format

Equations

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

Tau.BookVI.SelfDesc.instReprSelfDescPredicate

source instance Tau.BookVI.SelfDesc.instReprSelfDescPredicate :Repr SelfDescPredicate

Equations

  • Tau.BookVI.SelfDesc.instReprSelfDescPredicate = { reprPrec := Tau.BookVI.SelfDesc.instReprSelfDescPredicate.repr }

Tau.BookVI.SelfDesc.canonical_selfdesc

source def Tau.BookVI.SelfDesc.canonical_selfdesc :SelfDescPredicate

Equations

  • Tau.BookVI.SelfDesc.canonical_selfdesc = { condition_count := 3, count_eq := Tau.BookVI.SelfDesc.canonical_selfdesc._proof_1 } Instances For

Tau.BookVI.SelfDesc.InternalEvaluator

source structure Tau.BookVI.SelfDesc.InternalEvaluator :Type

[VI.D09] Internal evaluator: morphism in End(X), no oracle needed.

  • is_endomorphism : Bool
  • domain_in_carrier : Bool
  • no_oracle : Bool Instances For

Tau.BookVI.SelfDesc.instReprInternalEvaluator

source instance Tau.BookVI.SelfDesc.instReprInternalEvaluator :Repr InternalEvaluator

Equations

  • Tau.BookVI.SelfDesc.instReprInternalEvaluator = { reprPrec := Tau.BookVI.SelfDesc.instReprInternalEvaluator.repr }

Tau.BookVI.SelfDesc.instReprInternalEvaluator.repr

source def Tau.BookVI.SelfDesc.instReprInternalEvaluator.repr :InternalEvaluator → ℕ → Std.Format

Equations

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

Tau.BookVI.SelfDesc.internal_eval

source def Tau.BookVI.SelfDesc.internal_eval :InternalEvaluator

Equations

  • Tau.BookVI.SelfDesc.internal_eval = { } Instances For

Tau.BookVI.SelfDesc.code_reconstruction

source theorem Tau.BookVI.SelfDesc.code_reconstruction :internal_eval.no_oracle = true

[VI.P02] Code reconstruction: ω-germ code encodes distinction.

Tau.BookVI.SelfDesc.SelfDescClosure

source structure Tau.BookVI.SelfDesc.SelfDescClosure :Type

[VI.T03] SelfDesc Closure: SelfDesc pair is self-maintaining.

  • basin_correction : Bool
  • code_integrity : Bool
  • closure_under_eval : Bool Instances For

Tau.BookVI.SelfDesc.instReprSelfDescClosure

source instance Tau.BookVI.SelfDesc.instReprSelfDescClosure :Repr SelfDescClosure

Equations

  • Tau.BookVI.SelfDesc.instReprSelfDescClosure = { reprPrec := Tau.BookVI.SelfDesc.instReprSelfDescClosure.repr }

Tau.BookVI.SelfDesc.instReprSelfDescClosure.repr

source def Tau.BookVI.SelfDesc.instReprSelfDescClosure.repr :SelfDescClosure → ℕ → Std.Format

Equations

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

Tau.BookVI.SelfDesc.closure_thm

source def Tau.BookVI.SelfDesc.closure_thm :SelfDescClosure

Equations

  • Tau.BookVI.SelfDesc.closure_thm = { } Instances For

Tau.BookVI.SelfDesc.selfdesc_closure_theorem

source theorem Tau.BookVI.SelfDesc.selfdesc_closure_theorem :closure_thm.basin_correction = true ∧ closure_thm.code_integrity = true ∧ closure_thm.closure_under_eval = true

Tau.BookVI.SelfDesc.SevenHallmarksComplete

source structure Tau.BookVI.SelfDesc.SevenHallmarksComplete :Type

[VI.P04] Seven hallmarks complete: bijection H → F, H = F = 7.
  • hallmark_count : ℕ
  • count_eq : self.hallmark_count = 7
  • formal_count : ℕ
  • formal_eq : self.formal_count = 7
  • is_bijection : Bool Instances For

Tau.BookVI.SelfDesc.instReprSevenHallmarksComplete.repr

source def Tau.BookVI.SelfDesc.instReprSevenHallmarksComplete.repr :SevenHallmarksComplete → ℕ → Std.Format

Equations

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

Tau.BookVI.SelfDesc.instReprSevenHallmarksComplete

source instance Tau.BookVI.SelfDesc.instReprSevenHallmarksComplete :Repr SevenHallmarksComplete

Equations

  • Tau.BookVI.SelfDesc.instReprSevenHallmarksComplete = { reprPrec := Tau.BookVI.SelfDesc.instReprSevenHallmarksComplete.repr }

Tau.BookVI.SelfDesc.seven_hallmarks

source def Tau.BookVI.SelfDesc.seven_hallmarks :SevenHallmarksComplete

Equations

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

Tau.BookVI.SelfDesc.seven_hallmarks_complete

source theorem Tau.BookVI.SelfDesc.seven_hallmarks_complete :seven_hallmarks.hallmark_count = 7 ∧ seven_hallmarks.formal_count = 7 ∧ seven_hallmarks.is_bijection = true

Tau.BookVI.SelfDesc.life_requires_both

source theorem Tau.BookVI.SelfDesc.life_requires_both :canonical_selfdesc.condition_count = 3 ∧ Distinction.canonical_distinction.condition_count = 5

Life = Distinction AND SelfDesc.