THE ARMED SEAT

THE ARMED SEAT. Core Lean 4, standalone, no library. No axiom is declared anywhere in this file.

Once the seat is earned its denial is impossible by theorem, and this file says exactly what that means.

I · The deed. A proposition whose denial hands it over holds: SelfVerifying P is ¬P → P, and P follows

(opens_on_the_deed); the recursion is every proposition's (recursion_is_shared), so it discriminates nothing.

II · The root, self-grounding. A root R is self-grounding when acts occur and every act instances R. Then a denial

of R is an act and re-enacts R (denial_reenacts_root); an external proof adds nothing (external_proof_adds_nothing);

R is self-verifying (denial_instantiates) and held (seated_undeniable). The Root Axiom at the constructed one-point

domain is such a root (raSelfGrounding, root_undeniable).

III · The Omega guard. The denial that registers pays the floor, k_B T ln 2 per irreversibly registered bit, here an

exact integer in units of 10^-45 J; zero bits pay nothing; a reversibly held denial is charged nothing and commits

nothing; a temperature of zero prices nothing; the price is linear and monotone in bits.

IV · AEGIS. The refusal p(G) ≠ G is a constant function of the deed and never of the logic offered; every

adjudication is itself an act; four logics, one refusal, four deeds.

V · The scope of the armor. It covers the seat and the register, never the keyed bit: not every proposition is

self-verifying, and the line property's denial is a coherent frame in the Bridge. What cannot be denied is the

act of denying.

namespace Armed

/-! ## I · the deed -/

def SelfVerifying (P : Prop) : Prop := ¬P → P

/-- A self-verifying proposition holds: its lock opens on the deed of denying it. -/

theorem opens_on_the_deed (P : Prop) (utter : SelfVerifying P) : P :=

Classical.byContradiction (fun n => n (utter n))

/-- The recursion is shared by every proposition, so it discriminates nothing by itself. -/

theorem recursion_is_shared (P : Prop) : SelfVerifying P ↔ P :=

⟨fun h => Classical.byContradiction (fun n => n (h n)), fun p _ => p⟩

/-! ## II · the root, self-grounding -/

/-- A self-grounding root: acts occur, and every act instances the root. -/

structure SelfGrounding (R : Prop) where

Act : Type

anAct : Act

instances : Act → R

/-- A denial of the root is an act, and re-enacts it. -/

theorem denial_reenacts_root {R : Prop} (G : SelfGrounding R) (denial : G.Act) : R :=

G.instances denial

/-- An external proof of a self-grounding root adds nothing to it. -/

theorem external_proof_adds_nothing {R : Prop} (G : SelfGrounding R) (Q : Prop) : (Q → R) ↔ R :=

⟨fun _ => G.instances G.anAct, fun r _ => r⟩

/-- A self-grounding root is self-verifying: the deed of denying it hands it over. -/

theorem denial_instantiates {R : Prop} (G : SelfGrounding R) : SelfVerifying R :=

fun _ => G.instances G.anAct

/-- SEATED, UNDENIABLE: a self-grounding root holds, with no classical detour, by the act itself. -/

theorem seated_undeniable {R : Prop} (G : SelfGrounding R) : R :=

G.instances G.anAct

/-- The Root Axiom at the constructed one-point domain: every act is a deed, and a deed actuates. -/

def RA : Prop := (0 : Int) < 1

def raSelfGrounding : SelfGrounding RA := ⟨Unit, (), fun _ => show (0 : Int) < 1 by decide⟩

theorem root_undeniable : RA := seated_undeniable raSelfGrounding

/-! ## III · the Omega guard -/

/-- k_B · T · ln 2 in units of 10⁻⁴⁵ J: k_B = 1380649 · 10⁻²⁹ J/K exactly (SI 2019), ln 2 = 6931471805599453 · 10⁻¹⁶

to sixteen digits, the same constants the codex and the twin carry. -/

def landauerScaled (tkel bits : Nat) : Nat := bits * 1380649 * tkel * 6931471805599453

inductive OmegaCode | refused | noDenial | priced | reversible

deriving DecidableEq, Repr

/-- The Omega boundary: a temperature of zero prices nothing; zero bits register no denial; a reversibly held

denial is charged nothing and commits nothing; an irreversibly registered denial pays the floor. -/

def omegaBoundary (bits tkel : Nat) (irreversible : Bool) : OmegaCode × Nat :=

if tkel = 0 then (.refused, 0)

else if bits = 0 then (.noDenial, 0)

else if !irreversible then (.reversible, 0)

else (.priced, landauerScaled tkel bits)

/-- THE DENIAL PAYS THE FLOOR: one bit at 300 K, 2.870978885078723755499100 × 10⁻²¹ J, exact. -/

theorem omega_paid_floor : omegaBoundary 1 300 true = (.priced, 2870978885078723755499100) := by decide

theorem omega_zero_bits : omegaBoundary 0 300 true = (.noDenial, 0) := by decide

theorem omega_reversible_branch : omegaBoundary 1 300 false = (.reversible, 0) := by decide

theorem omega_refuses_zero_temp : ∀ b : Bool, omegaBoundary 1 0 b = (.refused, 0) := by decide

/-- The price is linear in the bits registered. -/

theorem omega_linear (n : Nat) : landauerScaled 300 n = n * landauerScaled 300 1 := by

unfold landauerScaled

omega

/-- And monotone: two bits pay more than one. -/

theorem omega_monotone : (omegaBoundary 1 300 true).2 < (omegaBoundary 2 300 true).2 := by decide

/-! ## IV · AEGIS -/

structure AegisState where

deeds : Nat

lastLen : Nat

deriving DecidableEq, Repr

def refusalConst : String :=

"p(G) /= G: precisification is an actuation, G is a non-actuation, and no logic makes a deed a non-deed"

/-- The guard reads the logic offered and consults only the act: the refusal never varies with the parameter. -/

def aegisGuard (logic : String) (s : AegisState) : String × AegisState :=

(refusalConst, ⟨s.deeds + 1, logic.utf8ByteSize⟩)

/-- THE REFUSAL IS CONSTANT: one refusal under every logic. -/

theorem aegis_constant (l₁ l₂ : String) (s : AegisState) : (aegisGuard l₁ s).1 = (aegisGuard l₂ s).1 := rfl

/-- Every adjudication is itself an act. -/

theorem aegis_deed_increments (l : String) (s : AegisState) : (aegisGuard l s).2.deeds = s.deeds + 1 := rfl

/-- The guard reads its parameter: the last logic's length is recorded, and the refusal still does not move. -/

theorem aegis_reads_parameter (l : String) (s : AegisState) : (aegisGuard l s).2.lastLen = l.utf8ByteSize := rfl

def fourLogics : AegisState :=

(aegisGuard "substructural"

(aegisGuard "fuzzy" (aegisGuard "paraconsistent" (aegisGuard "classical" ⟨0, 0⟩).2).2).2).2

/-- Four logics, classical, paraconsistent, fuzzy and substructural: four deeds counted, the last name read. -/

theorem aegis_four_logics : fourLogics.deeds = 4 ∧ fourLogics.lastLen = 13 := by decide

/-! ## V · the scope of the armor -/

/-- THE ARMOR COVERS THE ACT, NOT THE BIT. Every self-grounding root holds; and not every proposition is

self-verifying, so nothing is undeniable merely by being asserted. The keyed bit is contingent and stays free. -/

theorem armor_scope : (∀ (R : Prop) (_ : SelfGrounding R), R) ∧ ¬ (∀ P : Prop, SelfVerifying P) :=

⟨fun _ G => G.instances G.anAct, fun h => h False (fun x => x)⟩

/-! ## the armed seat, whole -/

/-- THE ARMED SEAT. The deed hands over what its denial denies; a self-grounding root is re-enacted by every act

against it, gains nothing from outside, and holds; the Root Axiom at the constructed domain is such a root; the

denial that registers pays the floor, exact, zero bits pay nothing, the reversible branch pays nothing, zero

temperature prices nothing, and the price is linear; the refusal is constant under every logic and every

adjudication is an act; and not every proposition is self-verifying, so the armor stops at the seat. -/

theorem armed :

(∀ P : Prop, SelfVerifying P → P) ∧

(∀ (R : Prop) (_ : SelfGrounding R) (Q : Prop), (Q → R) ↔ R) ∧

(∀ (R : Prop) (_ : SelfGrounding R), SelfVerifying R ∧ R) ∧

RA ∧

omegaBoundary 1 300 true = (.priced, 2870978885078723755499100) ∧

omegaBoundary 0 300 true = (.noDenial, 0) ∧

omegaBoundary 1 300 false = (.reversible, 0) ∧

(∀ b : Bool, omegaBoundary 1 0 b = (.refused, 0)) ∧

(∀ n : Nat, landauerScaled 300 n = n * landauerScaled 300 1) ∧

(∀ (l₁ l₂ : String) (s : AegisState), (aegisGuard l₁ s).1 = (aegisGuard l₂ s).1) ∧

(fourLogics.deeds = 4 ∧ fourLogics.lastLen = 13) ∧

¬ (∀ P : Prop, SelfVerifying P) :=

⟨opens_on_the_deed, fun _ G Q => external_proof_adds_nothing G Q,

fun _ G => ⟨denial_instantiates G, seated_undeniable G⟩, root_undeniable,

omega_paid_floor, omega_zero_bits, omega_reversible_branch, omega_refuses_zero_temp, omega_linear,

TRACTATUS VERITATIS TRISDUCTIVUS

THE ARMED SEAT

Topics

Archive