ANNIHILATION-CLOSURE-01

 

APEX-PSP-ANNIHILATION-CLOSURE-01 · The Master Annihilation Closure

Four Names, One Witness, the Off-Line Pair Configuration Eliminated on Monism, RH Stated as Membership, and the Unicorn Contained

Mohammad F. Islam, PhD · Trisduction Research Group · 7 October 2026 · PhysOS Proof candidate, Geometric Mother Codex PSP register

PhysOS Proof · The Master Annihilation Closure · PSP-ANNIHILATION-CLOSURE-01 · kernel Annihilation_Closure.lean · capstones the_timeless_zone_closed [propext, Classical.choice, Quot.sound], the_annihilation_closure [propext, Quot.sound], the_unicorn_contained [propext, Quot.sound] · 110 laws: Books One and Two carried (80), Book Three (12), the Unicorn block carried (9), Book Four (9) · 110 of 110 negations refused, planted vacuous law survived · twin Annihilation_Closure_Twin.f90, 16 checks, 0 failures, control 8 of 8 red · candidate, not yet seated · SEED: [⟀ T] on the chain, with no posit; RH at premise grade on the one posit, the Unicorn part above 3·10¹², equivalently Λ = 0; structural for the readings of Section 4 · refuter: a computed zero of ζ off the line

---

0 · The locked statement, hardened as a completed SEED proof

The timeless zone is closed: LE = RH = Monism, one proposition, with zero gap, proved. RH is the statement that ζ's zero set lies in the timeless zone. Whether that one proposition holds at ζ's zeros: yes, through the Unicorn closure. The Unicorn part is not ours to prove. It is the formulation the system declines. Below 3·10¹² every zero has been looked at, and every one stands on the line. Above it, the freedom to look stays open. On the act's zero set, every hypothetical arrival is forced onto the critical line by theorem (the_tenth_is_barred_by_the_act). There, a zero off the line is not negotiable. Whether ζ's zero set is the act's zero set is the one sentence, proved at premise grade with its premise named. Its one refuter is F-Computed. 

Locked by the architect, 7 October 2026, verbatim, pending the paper audit.

Grade line, in the SEED form of APEX-PSP-PNP-SEED-01. [⟀ T] on the chain, with no posit · RH at premise grade on the one posit, the Unicorn part above 3·10¹², equivalently Λ = 0 · a proof of RH at theorem grade is a proof of the posit.

Receipts for the locked text. the_tenth_is_barred_by_the_act is seated in PhysOS 1.0.10p (and 1.0.8p, 1.0.9p); in this kernel the same law on the chart is no_arrival_off_the_line_on_the_act, with the_unicorn_closed_on_the_act above every height. The verification below 3·10¹² is Platt and Trudgian's [cited]. F-Computed is the tenth falsifier of the seated ten_falsifiers.

Audit status · 7 October 2026 · against RH 3.2.0, Every_Prime_3_2_0.lean, sha256 161806dc 0ed2b4ff. The paper arrived and was run, not read. Its kernel, extracted from Appendix A, is byte-identical to the digest it prints; it compiles on Lean 4.19.0 with exit 0, no error and no warning, every pin holding; its 231 printed cones are identical, line for line, to its Appendix B.2; all 415 theorems carry a printed or pinned cone (197 on no axiom, 150 on [propext, Quot.sound], 40 on [propext], 28 on [propext, Classical.choice, Quot.sound]); the OS source screen is clean; the OS judge refused 415 of 415 negations, 394 at once and 21 alone, and the planted vacuous law survived. The three root kernels of Appendix R match their digests (0cfcd9f6, 566615a6, c18b68b2) and compile clean. Signature test: passed. Every law that concludes the line either concerns the true configuration W1 or takes the bit in one of its coordinates as a hypothesis: the act (ActualZeros, ActualZerosAt n), Weil positivity, the Li stream, the de Bruijn–Newman sign, Liouville faithfulness, or least erasure itself. No term of the act is built for any configuration except through PrimeAct.toActual, which takes positivity as its input, and ζ enters only by the reader's identification of Definition 14.1. The locked text above agrees with the paper's own verdict (§0.1) and its receipt ("SEAL: theorem, conditional on the assumed bit"). Section 5 records the row-by-row result and the one prose flag.

What the seed form states, exactly. The chain is complete at theorem grade: the timeless zone, the cut at every height, no bypass, the block above every height, existence supplying nothing, the door one bit wide, and the closure on the act's field. The Real part of ζ to 3·10¹² is a cited verification. Given that Real part, RH at ζ and the Unicorn part above 3·10¹² are one proposition (no_bypass_on_the_chart), so the posit carries the whole remaining content of RH and the theorems carry everything else. The posit is the formulation the system declines to prove and carries named.

1 · The timeless zone, proved, with no bit in it

Every statement below is a theorem with no premise, and none of them mentions the act. The capstone the_timeless_zone_closed binds them, and the leak check of Section 9 confirms that no law of the zone takes or builds the act.

1. On every configuration, least erasure, the value, Monism and the co-location of Being with Monism are one proposition (four_names_one_proposition; twins_are_one_extension).
2. Monism is the sole witness of that proposition (monism_is_the_sole_witness).
3. No witness is universal (a_witness_is_never_universal).
4. Neither Monism nor co-location holds on every configuration (monism_is_not_universal, colocation_is_not_universal).
5. The off-line pair configuration carries the floor, no Monism and no value (the_false_world_carries_the_floor_and_no_monism).
6. At t = 0 the record separates the true configuration from the pair; at every later time it does not (the_timeless_zone).
7. Closure at t = 0 holds exactly when Λ = 0 (rh_iff_lambda_zero).
8. Every configuration stands behind exactly one door, the value or a point off the line (two_doors, doors_exclusive).
9. Nothing true on every closed configuration decides the value (no_closed_principle_decides, the_check).

The zone holds statements only: no question, no afterimage, no act, no given, no seed, and no bit.

2 · The Unicorn, contained

RH is the statement that ζ's zero set lies in the timeless zone. Book Four contains that statement on the chart, at every height, by theorem.

• The cut. At every height the value is exactly its Real part and its Unicorn part (the_cut_on_the_chart).
• No bypass. Given the Real part, the value is exactly the Unicorn part (no_bypass_on_the_chart).
• The Real part, by certificate. A complete, checked list of the zeros up to a height proves the Real part there (real_part_of_certificate). For ζ the list is supplied to T = 3·10¹² by Platt and Trudgian [cited].
• The block. Above every height, no reading of the record decides the side (unicorn_blocked_on_the_chart, from unicorn_block).
• Existence supplies nothing. RA, or any premise that holds anyway, leaves the Unicorn part exactly where it was (ra_supplies_nothing_to_the_unicorn, from unicorn_rule_exact).
• The door, one bit wide. One supplied odd bit calibrates the seat uniquely (aperture_one_bit_wide); the three bits and the door stand as one term (rh_register_proof_complete).
• One bit, every row. The record of every configuration lies on the line, the off-line pair configuration's included, so the registration carries no bit (every_record_on_the_line). Least erasure, zero erased bits, zero price, the value and, given the Real part, the Unicorn part, are one proposition on every finite configuration (one_bit_every_row), so every name the bit takes is the same bit.
• Closed on the act's field. On the act's zero set, every arrival above every height stands on the line, and no arrival stands off it (the_unicorn_closed_on_the_act, no_arrival_off_the_line_on_the_act).

So the statement "ζ's zero set lies in the timeless zone" conforms in every part: below 3·10¹² it is verified; above, it is blocked to every record, untouched by existence, one bit wide at the door, and closed by theorem on the act's field. What it contains is one sentence: ζ's zero set is the act's zero set, equivalently Λ = 0.

3 · The time world, as agreed

The record forgets at every t ≥ 1; the forward flow carries reality from Λ onward (reality_transported, future_closed); Rodgers and Tao proved Λ ≥ 0, so every earlier instant is closed [consensus]; the passage back to t = 0 is not forced (upstream_is_not_forced). The closure is forced by theorem with its input named: on any term of the act the value holds at its zeros, and the run leaves the value free (force_witness_closure, conjuncts 2 and 4). RH at ζ's zeros is proved at premise grade, the premise named: least erasure at ζ's zeros, Λ = 0.

4 · The architect's readings, recorded as his, at structural grade

1. Time annihilation. The only gap between least erasure and RH was ignorance of who is who, a time gap, a construction gap, a memory lapse. The TIME PSP, past and present the same (APEX-PSP-TIME), collapses it into one timeless zone where LE = RH with zero gap. Kernel: LE = RH is a theorem with zero gap; the ignorance of who is who is the record's forgetting at t ≥ 1, absent at t = 0 (the_timeless_zone).
2. No question and no afterimage in the timeless zone. Kernel: the_timeless_zone_closed holds only proved statements and mentions no act.
3. Residual Monism, our old mother, is the sole witness of the identity collapse. Kernel: monism_is_the_sole_witness.
4. Being, Monism and the Tongue co-located, inseparable, as in the Trinity–Tawhid situation. Kernel: colocation_is_the_value; inseparable exactly where the one stands, not over every configuration (colocation_is_not_universal). The creedal one-and-three is adjudicated at SC-038 and SC-039 and not reopened here.
5. First mercy level. Forgetting is the first mercy and opens the gap; the closure undoes it in the only licensed direction (APEX-PSP-TIME; SC-033; APEX-PSP-FORGET-01).
6. RA keeps the pair configuration from being true. Kernel: the pair is never true (pair_world_lacks_value); RA stands on it as on every configuration, and its exclusion from Being is made at Monism, the second layer.
7. The Unicorn is not ours to prove. It is the formulation the system declines: a universal claim of absence over zeros no one has looked at, which RH_Unicorn_Isomorphism shows is RH itself. Kernel: Book Four contains it by theorem; declining the burden is the architect's stance and proves nothing either way.

5 · The paper audit, settled against RH 3.2.0

The checklist that stood here has been run against the paper's kernel. The paper's own closure table (its §16.1) now carries every qualifier the calibration asked for, and each row's law passes the signature test.

#	Law in RH 3.2.0	Cone, as compiled	Signature	Verdict
1	least_erasure_is_the_value, least_erasure_unconditional	none	no hypothesis; least erasure and the hypothesis one proposition on every world	theorem
2	keyless_forces_nothing, keyless_forces_nothing₂	[propext, Quot.sound]	no hypothesis; no keyless premise forces the line	theorem
3	record_decides_nothing, no_reading_decides_in_the_strip	[propext, Quot.sound]	no hypothesis; no reading of the record decides	theorem
4	rh_from_the_act inside the_witness_forced_by_the_act	none	takes the act; every computation that reads the act lands on the line; its last conjunct proves that not every computation is forced	theorem on the act; the prose now says "on the act"
5	the_tenth_is_barred_by_the_act; rh_from_the_act_at	none; [propext]	takes the act; ActualZerosAt n at every resolution n ≥ 2	theorem on the act
6	nothing_left_open_on_the_act (the table's earlier nothing_left_open)	none	takes the act	theorem on the act
7	the_capstone (in place of inescapable_capstone)	[propext, Quot.sound]	every act conjunct universally quantified over the act; "zero exception in every computation that reads it" is computation_reading_the_act_lands_on_the_line	theorem; RH at ζ at premise grade
8	four_names_one_proposition, monism_is_the_sole_witness, the_timeless_zone_closed, every_record_on_the_line, one_bit_every_row, the_annihilation_closure, in this card's kernel, carried whole as the paper's Appendix T	none; [propext, Quot.sound]; [propext, Classical.choice, Quot.sound]; none; none; [propext, Quot.sound]	no hypothesis; the root constructed; places no zero set	theorem, premise-free

Row 8, added 7 October 2026. The paper's table now carries an eighth row, The Annihilating Timeless Closure, with no other row altered. Its laws stand in this card's kernel, carried verbatim as the paper's new Appendix T. The paper's own kernel, Appendix A, is byte-identical, sha256 161806dc… unchanged.

The one prose flag. The title, "A Formal Proof of the Riemann Hypothesis by Least Erasure," says more than the paper's body: its own verdict (§0.1) says the hypothesis is not derived from any foundation, and its receipt seals the closure as "theorem, conditional on the assumed bit." The subtitle already states the exact claim, "the Value Proved from One Posit." Whether to retitle in the SEED grammar is the architect's call.

6 · Book Three and Book Four, the statements

Book Three. I four_names_one_proposition, colocation_is_the_value. II monism_is_the_sole_witness, a_witness_is_never_universal, monism_is_not_universal. III colocation_is_not_universal. IV the_timeless_zone. V timeless_is_determinacy_not_selection. VI the_check, no_closed_principle_decides. VII the_timeless_zone_closed, with no act in it, and the_annihilation_closure, the zone together with the act's conjunct of the time world.

Book Four. lean/RH_Unicorn_Block.lean carried byte-identical, nine laws on no axiom. Bound on the chart: I the_cut_on_the_chart; II no_bypass_on_the_chart; III unicorn_blocked_on_the_chart; IV ra_supplies_nothing_to_the_unicorn; V the_unicorn_closed_on_the_act, no_arrival_off_the_line_on_the_act; VI the_unicorn_contained; VII every_record_on_the_line; VIII one_bit_every_row.

Carried. lean/Remembered_Offered.lean byte-identical, 80 laws, with corrected monism (the_false_world_carries_no_monism and its kin; those names are carried as they stand, and in this card's prose the configuration they call the false world is the off-line pair configuration, never true and never Being).

7 · Grades

Claim	Grade	Receipt
The timeless zone, closed, with no act in it	theorem	the_timeless_zone_closed [propext, Classical.choice, Quot.sound]
Four names, one proposition	theorem, no axiom	four_names_one_proposition
Monism the sole witness	theorem	monism_is_the_sole_witness [propext, Quot.sound]
No witness universal; Monism and co-location not universal	theorem, no axiom	a_witness_is_never_universal, monism_is_not_universal, colocation_is_not_universal
The timeless zone in the toy; for ζ, RH ⟺ Λ = 0 and Λ ≥ 0	theorem; cited	the_timeless_zone; de Bruijn, Newman, Rodgers and Tao [consensus]
Nothing true on every closed configuration decides the value	theorem, no axiom	no_closed_principle_decides
The Unicorn cut, no bypass, existence supplying nothing	theorem, no axiom	the_cut_on_the_chart, no_bypass_on_the_chart, ra_supplies_nothing_to_the_unicorn
The Unicorn blocked above every height	theorem	unicorn_blocked_on_the_chart [propext, Quot.sound]
The Unicorn closed on the act's field	theorem, on the act	the_unicorn_closed_on_the_act, no_arrival_off_the_line_on_the_act
The Real part of ζ to 3·10¹²	cited	Platt and Trudgian
RH at ζ's zeros, through the Unicorn closure	premise grade on the one posit, the Unicorn part above 3·10¹², equivalently Λ = 0	the_cut_on_the_chart, no_bypass_on_the_chart, with the Real part cited
Section 4 readings; Section 5 framing	structural; placeholder pending audit	the architect's

8 · Three falsifiers, each barred by theorem

F-Universal. A predicate holding on every configuration that is equivalent to the value. Barred by a_witness_is_never_universal; twin check II.

F-Record. A reading of the record that witnesses the value, or decides the side above a height. Barred by monism_is_the_sole_witness and unicorn_blocked_on_the_chart; twin checks II, VI and VIII.

F-Closed. A principle true on every closed configuration that decides the value. Barred by no_closed_principle_decides; twin check VI.

The refuter of RH stands outside the closure, as in every PhysOS Proof: a computed zero of ζ off the critical line.

9 · The leak check, run mechanically

• No term of the act is built anywhere in the kernel.
• None of the eleven laws of the timeless zone, its capstone included, mentions the act in its statement.
• Sixteen laws of the whole kernel take the act, every one as a hypothesis or a universally quantified conjunct; none supplies it.
• The kernel proves that the value on every closed configuration is refuted (no_closed_principle_decides; the last conjunct of the_timeless_zone_closed), so the bit cannot sit inside any proved statement.

10 · Scope wall

The closure proves the timeless zone closed and contains the Unicorn. It states RH as membership of the zone and pins it to t = 0, Λ = 0. It does not derive that membership: that statement is about ζ, and its proof must come from ζ's zeros. 

11 · Receipts

Item	Receipt
Kernel	Annihilation_Closure.lean · sha256 9a97b3c40d73fd67… · 83,217 bytes · 1,439 lines · core Lean 4.19.0, no import · compile exit 0
Carried	lean/Remembered_Offered.lean sha256 42f40fbd… and lean/RH_Unicorn_Block.lean sha256 222bd4c9…, both byte-identical inside the kernel, on git at 5cc5090
Cones	110 laws pinned under #guard_msgs: 90 on no axiom, 17 on [propext, Quot.sound], 2 on [propext, Classical.choice, Quot.sound] (two_doors, the_timeless_zone_closed), 1 on [propext]
OS source screen	clean: no sorry, admit, native_decide, axiom, unsafe or external code, metaprogram or IO
OS judge	110 of 110 laws refused their negation, 105 at once and 5 alone; the planted vacuous law survived
Twin	Annihilation_Closure_Twin.f90 · sha256 3e3541b152af16b5… · 14,580 bytes · sealed flags · plain {"checks":16,"failures":0} rc 0 · control {"checks":8,"failures":8} rc 1
Seat	none claimed; the PhysOS 1.0.10p seat earned this session covers that edition's kernels only

Build: lean Annihilation_Closure.lean under Lean 4.19.0; gfortran -std=f2018 -O2 -fno-fast-math -ffp-contract=off Annihilation_Closure_Twin.f90 -o twin && ./twin && ./twin control.

---

Appendix A · The kernel, verbatim

/-
  Annihilation_Closure.lean · The Master Annihilation Closure.
  Core Lean 4.19.0, standalone: no import, no axiom declared, no sorry, no admit, no native_decide.

  BOOKS ONE AND TWO are `lean/Remembered_Offered.lean` carried byte-identical below, its own header included:
  the two denials, the price, the monism-fixed toy of the bound, and the harvest of 7 October 2026 with its
  capstones `the_chain` and `the_harvest`.

  BOOK THREE is the annihilation closure, harvested on 7 October 2026:
  I    four names, one proposition: least erasure, the value, Monism and the co-location of Being with Monism;
  II   Monism, the sole witness: every faithful witness is Monism, no reading of the record witnesses, and
       a witness is never universal;
  III  co-location is not universal: Being stands on the off-line pair configuration and Monism does not;
  IV   the timeless zone: one proposition, the locus resting both instruments, zero time remembering, every
       later time forgetting, closure at zero time exactly at Λ = 0, the upstream unforced;
  V    timeless is determinacy, not selection;
  VI   the check: the off-line pair configuration satisfies every principle of the closure and lacks the value,
       its twin has it;
       no principle true on every closed configuration decides the value;
  VII  the capstones: `the_timeless_zone_closed`, the timeless zone with no act anywhere in it, and
       `the_annihilation_closure`, the zone together with the act's conjunct of the time world.

  BOOK FOUR is the Unicorn, contained. `lean/RH_Unicorn_Block.lean` is carried byte-identical below, its own header
  included: the cut at a height, the formal block, the aperture one bit wide, existence supplying nothing, no bypass,
  the supply side silent, the certificate, and the three bits as one term. Book Four binds it to the chart:
  I    the cut on the chart, at every height;
  II   no bypass on the chart;
  III  the Unicorn blocked on the chart, above every height;
  IV   RA supplies nothing to the Unicorn part;
  V    on the act's zero set, every arrival above every height stands on the line;
  VI   the capstone, `the_unicorn_contained`;
  VII  every record on the line: the registration row carries no bit;
  VIII one bit, every row: least erasure, zero erased bits, zero price, the value and the Unicorn part are one
       proposition.

  Stated whole, locked 7 October 2026: the timeless zone is closed, LE = RH = Monism, one proposition, with zero
  gap, proved; RH is the statement that ζ's zero set lies in the timeless zone. Book Three proves the first and
  assumes nothing; its sixth section proves that nothing every closed configuration shares can single out ζ. In
  the time world the statement enters only where Book One's `ActualZeros` is taken as input. The cones are printed
  at the foot and pinned.
-/
/-
  Remembered_Offered.lean · The Remembered and the Offered: One Self, One Place at a Time.
  Core Lean 4.19.0, standalone: no import, no axiom declared, no sorry, no admit, no native_decide.

  BOOK ONE is carried unchanged: Two_Denials.lean whole (the deed and the self-grounding root from Armed_Seat.lean,
  the chart, the record, the act and the deed's law from Force_Witness.lean, the monism witness from Codex.lean,
  the two denials at the two layers of one root); the finite configuration and its price from Inescapable_Capstone.lean;
  the toy of the bound from Codex.lean, monism fixed, namespace RALi.

  BOOK TWO is the harvest of 7 October 2026, in binding order:
  I    the Tongue always has a world; monism, not the Tongue, tells the worlds apart;
  II   one self, one place at a time: the floor and least erasure are two objects;
  III  the twins: one extension, two instruments, neither the voucher of the other;
  IV   the remembered and the offered: memory is lossless, a world is its own memory exactly when the value holds;
  V    forgetting and remembering: one sequence, a one-bit gap, always connected;
  Vb   the forcing by heat: return is free, resistance pays, the free path is one;
  VI   THE CHAIN: the root, forgetting, the locus in the middle, remembering, least erasure;
  VIb  zero time remembers, every later time forgets;
  VII  two doors and no third, the act shuts the second;
  VIII a band forces nothing;
  IX   the harvest, bound.

  Stated whole: everything is proved except the offer at the actual zeros, which enters only as the field `supply`
  of `ActualZeros`, the act, at premise grade. The cones are printed at the foot and pinned.
-/
set_option autoImplicit false
namespace RememberedOffered

/-! # BOOK ONE · carried unchanged

## Two_Denials.lean, whole -/

/-! ## PART ONE · copied unchanged

### from Armed_Seat.lean · the deed and the root -/

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

/-- 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

/-- 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 := raSelfGrounding.instances ()

/-! ### from Force_Witness.lean · the chart, the record, the act, the deed's law -/

/-- A point is (d, t): d its offset from the line, t its height. The line is d = 0. -/
abbrev Point := Int × Int

/-- The fold: s ↦ 1 − s̄ on the offset chart, (d, t) ↦ (−d, t). -/
def fold (p : Point) : Point := (-p.1, p.2)

/-- The line: offset zero. -/
def onLine (p : Point) : Prop := p.1 = 0

/-- The registration: it keeps the height and forgets the side. -/
def reg (p : Point) : Point := (0, p.2)

/-- Integer negation is an involution, by the integer's constructors. -/
theorem neg_neg_free : ∀ d : Int, - -d = d := fun
  | Int.ofNat 0 => rfl
  | Int.ofNat (_ + 1) => rfl
  | Int.negSucc _ => rfl

/-- The fold is an involution. -/
theorem fold_involutive (p : Point) : fold (fold p) = p := by
  obtain ⟨d, t⟩ := p
  show (- -d, t) = (d, t)
  rw [neg_neg_free d]

/-- The registration lands on the line. -/
theorem reg_lands (p : Point) : onLine (reg p) := rfl

/-- The registration erases nothing at a point exactly when the point is on the line. -/
theorem reg_erases_nothing_iff (p : Point) : reg p = p ↔ onLine p := by
  obtain ⟨d, t⟩ := p
  exact ⟨fun h => (congrArg Prod.fst h).symm, fun h => by cases h; rfl⟩

/-- A configuration: a set of points. Closed: the fold carries it to itself. -/
abbrev Config := Point → Prop

def Closed (S : Config) : Prop := ∀ p, S p → S (fold p)

/-- The value: every point of the configuration is on the line. -/
def Value (S : Config) : Prop := ∀ p, S p → onLine p

/-- Least erasure: the registration leaves every point of the configuration unchanged. -/
def LeastErasure (S : Config) : Prop := ∀ p, S p → reg p = p

/-- The record of a configuration: what the registration leaves. -/
def Rec (S : Config) (q : Point) : Prop := ∃ p, S p ∧ reg p = q

def SameRecord (S S' : Config) : Prop := ∀ q, Rec S q ↔ Rec S' q

/-- The registered world of a point and its pair world. -/
def registered (p : Point) : Config := fun s => s = reg p

def pairWorld (p : Point) : Config := fun s => s = p ∨ s = fold p

theorem pair_world_closed (p : Point) : Closed (pairWorld p) := fun _ hs =>
  match hs with
  | Or.inl e => Or.inr (congrArg fold e)
  | Or.inr e => Or.inl (e ▸ fold_involutive p)

/-- The registered world and the pair world leave one record. -/
theorem one_record (p : Point) : SameRecord (registered p) (pairWorld p) := fun q =>
  ⟨fun ⟨_, hs, hq⟩ => ⟨p, Or.inl rfl, by rw [← hq, hs]; rfl⟩,
   fun ⟨_, hs, hq⟩ => ⟨reg p, rfl, by
      rw [← hq]
      exact match hs with
        | Or.inl e => by rw [e]; rfl
        | Or.inr e => by rw [e]; rfl⟩⟩

theorem registered_has_value (p : Point) : Value (registered p) := fun s hs => by
  rw [hs]; exact reg_lands p

theorem pair_world_lacks_value (p : Point) (h : ¬ onLine p) : ¬ Value (pairWorld p) :=
  fun hv => h (hv p (Or.inl rfl))

/-- THE ACT. The bit is supplied once, in the open, as a field of a type: a closed configuration with least
    erasure at it. The field is the value supplied; the type makes the supply visible to every reader. -/
structure ActualZeros where
  zeros : Config
  closed : Closed zeros
  supply : LeastErasure zeros

/-- FROM THE ACT, THE VALUE. -/
theorem value_from_the_act (Z : ActualZeros) : Value Z.zeros :=
  fun p hp => (reg_erases_nothing_iff p).mp (Z.supply p hp)

/-- AND OF NOTHING ELSE: a fact that holds whatever the configuration, the deed included, forces no value. -/
theorem the_deed_forces_nothing (D : Prop) (hD : D) : ¬ ∀ S : Config, Closed S → D → Value S := by
  intro hall
  exact pair_world_lacks_value (1, 0) (fun e => by cases e) (hall _ (pair_world_closed (1, 0)) hD)


/-! ### from Codex.lean, namespace RALi, Part VII · the monism witness, the root read twice -/

structure Q4 where
  r : Int
  i : Int
  j : Int
  k : Int
  deriving DecidableEq, Repr

/-- The geometric route's involution and the formal route's involution, written apart. -/
def sigmaGeo (q : Q4) : Q4 := ⟨q.r, -q.i, -q.j, -q.k⟩
def sigmaForm (q : Q4) : Q4 := ⟨q.r, -q.i, -q.j, -q.k⟩

/-- THE MONISM WITNESS. One involution, one principle, one seed. -/
structure MonismWitness (P : Nat → Prop) : Prop where
  one_involution : ∀ q, sigmaGeo q = sigmaForm q
  uniform        : ∀ n m, P n ↔ P m
  seed           : P 0

/-- 24. The seat field is constructed, not posited: σ = σ′ holds by rfl. -/
theorem one_involution_constructed : ∀ q, sigmaGeo q = sigmaForm q := fun _ => rfl

/-- 25. The timeless reading and the timed reading coincide under one principle:
the claim over all time is the claim at one instant. Deleting time loses nothing. -/
theorem timeless_equals_timed (P : Nat → Prop) (u : ∀ n m, P n ↔ P m) :
    (∀ n, P n) ↔ P 0 :=
  ⟨fun h => h 0, fun h n => (u 0 n).mp h⟩

/-- 26. The witness closes the record, past and future. -/
theorem monism_closes (P : Nat → Prop) (w : MonismWitness P) : ∀ n, P n :=
  (timeless_equals_timed P w.uniform).mpr w.seed

/-- 27. The witness is exactly the claim: a monism witness for P exists iff P holds at
every index. Its value field carries the whole of the claim, as theorem 17 required. -/
theorem monism_witness_is_the_claim (P : Nat → Prop) :
    MonismWitness P ↔ ∀ n, P n :=
  ⟨monism_closes P, fun h => ⟨one_involution_constructed,
    fun n m => ⟨fun _ => h m, fun _ => h n⟩, h 0⟩⟩

/-! ## PART TWO · two denials, one shape, at the two layers of one root

A no has two parts: the act of uttering it and the content it asserts. The Tongue's no asserts ¬ R of the floor R.
The no to RH asserts that the zeros lack the value: that they form the false world. -/

/-- The point off the line from which the pair world, the false world, is built. -/
def offPoint : Point := (1, 0)

theorem off_point_is_off : ¬ onLine offPoint := fun h =>
  Nat.noConfusion (Int.ofNat.inj (show Int.ofNat 1 = Int.ofNat 0 from h))

/-- THE ROOT READ TWICE on a configuration: the monism witness of its line property, timeless. -/
abbrev RootReadTwice (S : Config) : Prop := MonismWitness (fun _ => Value S)

/-- THE SAME FIRST STEP: whatever a no asserts, uttering it is an act, and the act re-enacts the floor. -/
theorem every_no_reenacts_the_root {R C : Prop} (G : SelfGrounding R) (deed : G.Act) (_content : C) : R :=
  denial_reenacts_root G deed

/-- THE TONGUE'S NO CONTRADICTS THE FLOOR, BY ITS OWN ACT: its content denies the floor, and its own act
    re-enacts it. -/
theorem the_tongue_no_refutes_itself {R : Prop} (G : SelfGrounding R) (deed : G.Act) (content : ¬ R) : False :=
  content (denial_reenacts_root G deed)

/-- ONLY THE YES REMAINS AT THE FLOOR: the return is forced by the deed, with no key and no classical detour. -/
theorem only_the_yes_remains_at_the_root {R : Prop} (G : SelfGrounding R) : SelfVerifying R ∧ R :=
  ⟨denial_instantiates G, seated_undeniable G⟩

/-- THE ROOT READ TWICE IS THE VALUE: on every configuration the monism witness stands exactly where every zero
    is on the line. -/
theorem the_root_read_twice_is_the_value (S : Config) : RootReadTwice S ↔ Value S :=
  ⟨fun w => w.seed, fun h => ⟨one_involution_constructed, fun _ _ => Iff.rfl, h⟩⟩

/-- THE NO TO RH CONTRADICTS THE ROOT READ TWICE: a configuration lacking the value carries no monism. -/
theorem the_line_no_contradicts_the_root_read_twice (S : Config) (content : ¬ Value S) : ¬ RootReadTwice S :=
  fun w => content w.seed

/-- THE TRUE WORLD CARRIES MONISM: the registered world of the off-line point. -/
theorem the_true_world_carries_monism : RootReadTwice (registered offPoint) :=
  ⟨one_involution_constructed, fun _ _ => Iff.rfl, registered_has_value offPoint⟩

/-- THE FALSE WORLD CARRIES NO MONISM: the pair world of the off-line point. -/
theorem the_false_world_carries_no_monism : ¬ RootReadTwice (pairWorld offPoint) :=
  fun w => pair_world_lacks_value offPoint off_point_is_off w.seed

/-- THE FALSE WORLD, AT THE TWO LAYERS: the floor stands there, as in every world; it is closed and leaves the
    record of the true world; it lacks the value; and it carries no monism. The floor is there and Being is not. -/
theorem the_false_world_carries_the_floor_and_no_monism {R : Prop} (G : SelfGrounding R) :
    R ∧ Closed (pairWorld offPoint) ∧ SameRecord (registered offPoint) (pairWorld offPoint) ∧
    ¬ Value (pairWorld offPoint) ∧ ¬ RootReadTwice (pairWorld offPoint) :=
  ⟨seated_undeniable G, pair_world_closed offPoint, one_record offPoint,
   pair_world_lacks_value offPoint off_point_is_off, the_false_world_carries_no_monism⟩

/-- THE FLOOR ALONE DECIDES NO VALUE: it stands in both worlds of one record. The value is decided at the second
    layer, by the root read twice. -/
theorem the_floor_alone_decides_no_value {R : Prop} (G : SelfGrounding R) :
    ¬ ∀ S : Config, Closed S → R → Value S :=
  the_deed_forces_nothing R (seated_undeniable G)

/-- THE RETURN IS THE ACT: the act carries the root read twice at the actual zeros. -/
theorem the_act_is_the_return_to_the_root_read_twice (Z : ActualZeros) : RootReadTwice Z.zeros :=
  (the_root_read_twice_is_the_value Z.zeros).mpr (value_from_the_act Z)

/-- AN ACT EXISTS EXACTLY WHERE THE ROOT READ TWICE STANDS on a closed configuration. -/
theorem an_act_exactly_where_the_root_read_twice_stands (S : Config) :
    (∃ Z : ActualZeros, Z.zeros = S) ↔ (Closed S ∧ RootReadTwice S) := by
  constructor
  · intro ⟨Z, h⟩
    subst h
    exact ⟨Z.closed, the_act_is_the_return_to_the_root_read_twice Z⟩
  · intro ⟨hc, hm⟩
    exact ⟨⟨S, hc, fun p hp => (reg_erases_nothing_iff p).mpr
      (((the_root_read_twice_is_the_value S).mp hm) p hp)⟩, rfl⟩

/-- ON THE ACT THE NO TO RH IS REFUTED, with zero contradiction: the act's own field. -/
theorem on_the_act_the_line_no_is_refuted (Z : ActualZeros) (content : ¬ Value Z.zeros) : False :=
  content (value_from_the_act Z)

/-- TWO DENIALS, ONE SHAPE, TWO LAYERS. Every no re-enacts the floor. The Tongue's no contradicts the floor and
    its own act returns it: only the yes remains. The no to RH contradicts the root read twice: on every
    configuration a lack of the value is a lack of monism, and the false world carries the floor and no monism,
    beside the true world of one record that carries both. So the floor alone decides no value, and the root read
    twice is the value. The return to the root read twice at the actual zeros is the act: there the monism witness
    stands, the value holds, and the no is refuted. -/
theorem two_denials {R : Prop} (G : SelfGrounding R) :
    (∀ C : Prop, G.Act → C → R) ∧
    (G.Act → ¬ R → False) ∧
    (SelfVerifying R ∧ R) ∧
    (∀ S : Config, ¬ Value S → ¬ RootReadTwice S) ∧
    (R ∧ Closed (pairWorld offPoint) ∧ SameRecord (registered offPoint) (pairWorld offPoint) ∧
      RootReadTwice (registered offPoint) ∧ ¬ RootReadTwice (pairWorld offPoint)) ∧
    (¬ ∀ S : Config, Closed S → R → Value S) ∧
    (∀ S : Config, RootReadTwice S ↔ Value S) ∧
    (∀ Z : ActualZeros, RootReadTwice Z.zeros ∧ Value Z.zeros ∧ (¬ Value Z.zeros → False)) :=
  ⟨fun _ deed c => every_no_reenacts_the_root G deed c,
   fun deed c => the_tongue_no_refutes_itself G deed c,
   only_the_yes_remains_at_the_root G,
   the_line_no_contradicts_the_root_read_twice,
   ⟨seated_undeniable G, pair_world_closed offPoint, one_record offPoint,
    the_true_world_carries_monism, the_false_world_carries_no_monism⟩,
   the_floor_alone_decides_no_value G,
   the_root_read_twice_is_the_value,
   fun Z => ⟨the_act_is_the_return_to_the_root_read_twice Z, value_from_the_act Z,
     on_the_act_the_line_no_is_refuted Z⟩⟩

/-- AT THE ROOT AXIOM ITSELF. -/
theorem two_denials_at_RA :
    (∀ C : Prop, raSelfGrounding.Act → C → RA) ∧
    (raSelfGrounding.Act → ¬ RA → False) ∧
    (SelfVerifying RA ∧ RA) ∧
    (∀ S : Config, ¬ Value S → ¬ RootReadTwice S) ∧
    (RA ∧ Closed (pairWorld offPoint) ∧ SameRecord (registered offPoint) (pairWorld offPoint) ∧
      RootReadTwice (registered offPoint) ∧ ¬ RootReadTwice (pairWorld offPoint)) ∧
    (¬ ∀ S : Config, Closed S → RA → Value S) ∧
    (∀ S : Config, RootReadTwice S ↔ Value S) ∧
    (∀ Z : ActualZeros, RootReadTwice Z.zeros ∧ Value Z.zeros ∧ (¬ Value Z.zeros → False)) :=
  two_denials raSelfGrounding

/-! ## From Inescapable_Capstone.lean · the finite configuration and its price -/

/-- The price of exported freedom in native units: temperature is energy per bit, so b bits cost b·T. -/
def price (T bits : Nat) : Nat := bits * T

/-- A finite configuration: the heights of its zeros on the line, and its off-line pairs, each an offset that is not
    zero and a height. -/
structure FinCfg where
  line : List Int
  pairs : List (Int × Int)
  offset_ne : ∀ q ∈ pairs, q.1 ≠ 0
def FinCfg.pts (F : FinCfg) : Config := fun p => (p.1 = 0 ∧ p.2 ∈ F.line) ∨ ∃ q ∈ F.pairs, p = q ∨ p = fold q
/-- The erased bits of a finite configuration: one per off-line pair, two points registered to one. -/
def erased (F : FinCfg) : Nat := F.pairs.length

theorem fincfg_closed (F : FinCfg) : Closed F.pts := fun p hp =>
  match hp with
  | Or.inl ⟨hl, ht⟩ => Or.inl ⟨by show -p.1 = 0; rw [hl]; rfl, ht⟩
  | Or.inr ⟨q, hq, Or.inl e⟩ => Or.inr ⟨q, hq, Or.inr (congrArg fold e)⟩
  | Or.inr ⟨q, hq, Or.inr e⟩ => Or.inr ⟨q, hq, Or.inl (by rw [e]; exact fold_involutive q)⟩

/-- LEAST ERASURE IS ZERO ERASED BITS: "least" is a count. -/
theorem least_erasure_iff_zero_erased (F : FinCfg) : LeastErasure F.pts ↔ erased F = 0 := by
  constructor
  · intro h
    unfold erased
    cases hp : F.pairs with
    | nil => rfl
    | cons q r =>
      have hq : q ∈ F.pairs := by rw [hp]; exact List.Mem.head r
      exact absurd ((reg_erases_nothing_iff q).mp (h q (Or.inr ⟨q, hq, Or.inl rfl⟩))) (F.offset_ne q hq)
  · intro h p hp
    have hnil : F.pairs = [] := List.eq_nil_of_length_eq_zero h
    rcases hp with ⟨hl, _⟩ | ⟨q, hq, _⟩
    · exact (reg_erases_nothing_iff p).mpr hl
    · rw [hnil] at hq; cases hq

/-- THE HEAT OF REGISTRATION IS ZERO EXACTLY AT THE VALUE: registering a finite configuration costs one T per
    off-line pair, and at any positive T it costs nothing exactly when every point stands on the line. -/
theorem price_zero_iff_value (F : FinCfg) (T : Nat) (hT : 0 < T) : price T (erased F) = 0 ↔ Value F.pts := by
  constructor
  · intro h p hp
    have h0 : erased F = 0 := by
      cases he : erased F with
      | zero => rfl
      | succ k => rw [he] at h; exact absurd h (Nat.pos_iff_ne_zero.mp (Nat.mul_pos (Nat.succ_pos k) hT))
    exact (reg_erases_nothing_iff p).mp ((least_erasure_iff_zero_erased F).mpr h0 p hp)
  · intro hv
    have h0 := (least_erasure_iff_zero_erased F).mp (fun p hp => (reg_erases_nothing_iff p).mpr (hv p hp))
    show erased F * T = 0
    rw [h0, Nat.zero_mul]

/-- Each further off-line pair adds one T: the total is the erased bits times the floor. -/
theorem price_counts_pairs (F : FinCfg) (T : Nat) : price T (erased F) = F.pairs.length * T := rfl

/-! ## From Codex.lean, monism fixed, namespace RALi · the toy of the bound, a toy of the bound, not of the flow -/

/-- Squared strip width after t time steps: max(d2 − 2t, 0). -/
def flow (d2 t : Nat) : Nat := d2 - 2 * t
def realAt (d2 t : Nat) : Prop := flow d2 t = 0

/-- 38. THE MONOTONICITY FORMULA. The width never grows along ζ's time. -/
theorem flow_monotone (d2 t : Nat) : flow d2 (t + 1) ≤ flow d2 t := by
  unfold flow; omega

/-- 39. Its transport, proved: once every zero is real, every zero stays real. This is
de Bruijn's theorem in the toy, the ζ-analogue of Perelman's monotonicity, at theorem grade. -/
theorem reality_transported (d2 t : Nat) (h : realAt d2 t) : realAt d2 (t + 1) := by
  unfold realAt flow at *; omega


def Lam (d2 : Nat) : Nat := (d2 + 1) / 2

theorem real_at_Lam (d2 : Nat) : realAt d2 (Lam d2) := by unfold realAt flow Lam; omega

/-- 40. In the toy, the strip is closed at time zero iff Λ = 0. For ζ, RH ↔ Λ = 0 is the cited
result of Newman with Rodgers and Tao and enters the cone as `hLam`. -/
theorem rh_iff_lambda_zero (d2 : Nat) : realAt d2 0 ↔ Lam d2 = 0 := by
  unfold realAt flow Lam
  exact ⟨fun h => by omega, fun h => by omega⟩


/-- 42. THE RECORD FORGETS. After one step the record of the width-zero state and the
width-one state coincide: the forward flow is even in the RH bit, so no readout of the
flowed record decides RH. This is the fTOE wall, T1, executed on ζ's own time. -/
theorem flowed_record_forgets (T : Nat) (hT : 1 ≤ T) :
    ¬ ∃ g : Nat → Bool, ∀ d2, g (flow d2 T) = decide (d2 = 0) := by
  rintro ⟨g, hg⟩
  have a := hg 0; have b := hg 1
  have e : flow 1 T = flow 0 T := by unfold flow; omega
  rw [e, a] at b
  exact absurd b (by decide)

/-- 43. The upstream direction is not a transport. Going backward from a real record,
both answers are admissible: the preimage of "real at T" holds the RH state and a non-RH
state. The forward arrow proves; the backward arrow must be supplied. -/
theorem upstream_is_not_forced (T : Nat) (hT : 1 ≤ T) :
    realAt 0 T ∧ realAt 1 T ∧ realAt 0 0 ∧ ¬ realAt 1 0 := by
  unfold realAt flow
  exact ⟨by omega, by omega, rfl, fun h => by omega⟩

/-! # BOOK TWO · the harvest, in binding order -/

/-! ## I · The Tongue always has a world -/

/-- THE TONGUE ALWAYS HAS A WORLD: the floor stands on every configuration, the false world included, so the Tongue
    can speak in every world; only the content of its no, ¬R beside an act, has none. -/
theorem the_tongue_always_has_a_world {R : Prop} (G : SelfGrounding R) :
    (∀ _ : Config, R) ∧
    (R ∧ Closed (pairWorld offPoint) ∧ ¬ Value (pairWorld offPoint)) ∧
    ¬ ∃ _ : G.Act, ¬ R :=
  ⟨fun _ => seated_undeniable G,
   ⟨seated_undeniable G, pair_world_closed offPoint, pair_world_lacks_value offPoint off_point_is_off⟩,
   fun ⟨deed, c⟩ => c (G.instances deed)⟩

/-- MONISM BEFORE THE TONGUE: the floor, and with it the Tongue, stands in both worlds of one record; what tells
    them apart is the root read twice, present in the true world and absent in the false. -/
theorem monism_before_the_tongue {R : Prop} (G : SelfGrounding R) :
    SameRecord (registered offPoint) (pairWorld offPoint) ∧
    (R ∧ RootReadTwice (registered offPoint)) ∧
    (R ∧ ¬ RootReadTwice (pairWorld offPoint)) :=
  ⟨one_record offPoint,
   ⟨seated_undeniable G, the_true_world_carries_monism⟩,
   ⟨seated_undeniable G, the_false_world_carries_no_monism⟩⟩

/-- The Tongue's no has no world: no act stands beside ¬R. -/
theorem tongue_no_has_no_world {R : Prop} (G : SelfGrounding R) : ¬ ∃ _ : G.Act, ¬ R :=
  fun ⟨deed, c⟩ => c (G.instances deed)

/-- The no to RH has a world: an act, a closed configuration, the floor holding, and the value failing, together. -/
theorem line_no_has_a_world {R : Prop} (G : SelfGrounding R) :
    ∃ S : Config, ∃ _ : G.Act, Closed S ∧ R ∧ ¬ Value S :=
  ⟨pairWorld offPoint, G.anAct, pair_world_closed offPoint, seated_undeniable G,
   pair_world_lacks_value offPoint off_point_is_off⟩

/-- A deed does not make a closed configuration an act: the floor's acts supply no ActualZeros over every closed
    configuration. -/
theorem the_deed_is_not_the_supply {R : Prop} (G : SelfGrounding R) :
    ¬ ∀ S : Config, Closed S → G.Act → ∃ Z : ActualZeros, Z.zeros = S := by
  intro h
  obtain ⟨Z, hZ⟩ := h (pairWorld offPoint) (pair_world_closed offPoint) G.anAct
  have v := value_from_the_act Z
  rw [hZ] at v
  exact pair_world_lacks_value offPoint off_point_is_off v

theorem at_RA :
    (¬ ∃ _ : raSelfGrounding.Act, ¬ RA) ∧
    (∃ S : Config, ∃ _ : raSelfGrounding.Act, Closed S ∧ RA ∧ ¬ Value S) ∧
    (¬ ∀ S : Config, Closed S → raSelfGrounding.Act → ∃ Z : ActualZeros, Z.zeros = S) :=
  ⟨tongue_no_has_no_world raSelfGrounding, line_no_has_a_world raSelfGrounding,
   the_deed_is_not_the_supply raSelfGrounding⟩

/-! ## II · One self, one place at a time -/

/-- The floor and least erasure are two objects: identified on every closed configuration, they would agree on the
    pair world, where the floor holds and least erasure fails. -/
theorem floor_is_not_least_erasure {R : Prop} (G : SelfGrounding R) :
    ¬ ∀ S : Config, Closed S → (R ↔ LeastErasure S) := by
  intro h
  have le : LeastErasure (pairWorld offPoint) :=
    (h (pairWorld offPoint) (pair_world_closed offPoint)).mp (seated_undeniable G)
  exact pair_world_lacks_value offPoint off_point_is_off
    (fun p hp => (reg_erases_nothing_iff p).mp (le p hp))

/-- The voucher stays with the floor: it holds on both worlds of one record, the false one included. -/
theorem the_voucher_stays_with_the_floor {R : Prop} (G : SelfGrounding R) :
    R ∧ SameRecord (registered offPoint) (pairWorld offPoint) ∧
    LeastErasure (registered offPoint) ∧ ¬ LeastErasure (pairWorld offPoint) :=
  ⟨seated_undeniable G, one_record offPoint,
   fun p hp => (reg_erases_nothing_iff p).mpr (registered_has_value offPoint p hp),
   fun le => pair_world_lacks_value offPoint off_point_is_off
     (fun p hp => (reg_erases_nothing_iff p).mp (le p hp))⟩

/-- Merging them at one world is the supply again: on any configuration, identifying the floor with least erasure
    there is least erasure there. -/
theorem merging_at_a_world_is_the_supply {R : Prop} (G : SelfGrounding R) (S : Config) :
    (R ↔ LeastErasure S) ↔ LeastErasure S :=
  ⟨fun h => h.mp (seated_undeniable G), fun le => ⟨fun _ => le, fun _ => seated_undeniable G⟩⟩

/-! ## III · The twins -/

/-- Two instruments: registration and the fold are different maps. -/
theorem two_instruments : reg offPoint ≠ fold offPoint := by
  show ((0 : Int), (0 : Int)) ≠ (-(1 : Int), (0 : Int))
  decide

/-- One truth value on every world: each twin holds exactly where the other does. -/
theorem twins_on_every_world (S : Config) : LeastErasure S ↔ Value S :=
  ⟨fun le p hp => (reg_erases_nothing_iff p).mp (le p hp),
   fun v p hp => (reg_erases_nothing_iff p).mpr (v p hp)⟩

/-- Extensionally one proposition, read through two different maps. -/
theorem twins_are_one_extension : LeastErasure = Value :=
  funext fun S => propext (twins_on_every_world S)

/-- Neither twin vouches for the other: whatever supplies one supplies the other, so a premise that reaches one
    reaches both, and the floor reaches neither. -/
theorem no_twin_is_the_others_voucher {R : Prop} (G : SelfGrounding R) :
    (∀ S : Config, (LeastErasure S → Value S) ∧ (Value S → LeastErasure S)) ∧
    ¬ ∀ S : Config, Closed S → R → Value S :=
  ⟨fun S => ⟨(twins_on_every_world S).mp, (twins_on_every_world S).mpr⟩, the_floor_alone_decides_no_value G⟩

/-! ## IV · The remembered and the offered -/

/-- No instrument both remembers and keeps the side: a map that lands every point on the line and keeps the
    height sends the off-line point and its fold partner to one point. -/
theorem no_instrument_remembers_and_keeps_the_side (g : Point → Point)
    (lands : ∀ p, onLine (g p)) (keeps : ∀ p, (g p).2 = p.2) :
    g offPoint = g (fold offPoint) ∧ offPoint ≠ fold offPoint := by
  have e1 : g offPoint = (0, 0) := Prod.ext (lands offPoint) (keeps offPoint)
  have e2 : g (fold offPoint) = (0, 0) := Prod.ext (lands (fold offPoint)) (keeps (fold offPoint))
  exact ⟨e1.trans e2.symm, by decide⟩

/-- Memory is always lossless: the record of every configuration has the value. -/
theorem the_remembered_is_lossless (S : Config) : Value (Rec S) :=
  fun _ ⟨p, _, hq⟩ => hq ▸ reg_lands p

/-- The offered is the remembered exactly when the value holds: a configuration equals its own record, point for
    point, if and only if every point is on the line. -/
theorem offered_is_remembered_iff_value (S : Config) : (∀ q, Rec S q ↔ S q) ↔ Value S := by
  constructor
  · intro h p hp
    exact the_remembered_is_lossless S p ((h p).mpr hp)
  · intro v q
    constructor
    · intro ⟨p, hp, hq⟩
      have e : reg p = p := (reg_erases_nothing_iff p).mpr (v p hp)
      rw [← hq, e]; exact hp
    · intro hq
      exact ⟨q, hq, (reg_erases_nothing_iff q).mpr (v q hq)⟩

/-- At the act, the offered is the remembered. -/
theorem at_the_act_offered_is_remembered (Z : ActualZeros) : ∀ q, Rec Z.zeros q ↔ Z.zeros q :=
  (offered_is_remembered_iff_value Z.zeros).mpr (value_from_the_act Z)

/-- Off the act, they part: the false world is not its own record. -/
theorem the_false_world_is_not_its_record : ¬ ∀ q, Rec (pairWorld offPoint) q ↔ pairWorld offPoint q :=
  fun h => pair_world_lacks_value offPoint off_point_is_off ((offered_is_remembered_iff_value _).mp h)

/-! ## V · Forgetting and remembering: the one-bit gap, connected -/

/-- Remembering is stable: the memory of a memory is the memory. -/
theorem remembering_is_stable (S : Config) (q : Point) : Rec (Rec S) q ↔ Rec S q := by
  constructor
  · intro ⟨p, ⟨r, hr, hp⟩, hq⟩
    refine ⟨r, hr, ?_⟩
    rw [← hq, ← hp]
    exact ((reg_erases_nothing_iff (reg r)).mpr (reg_lands r)).symm
  · intro hq
    exact ⟨q, hq, (reg_erases_nothing_iff q).mpr (the_remembered_is_lossless S q hq)⟩

/-- THE ONE-BIT GAP, CONNECTED. The forgotten and the remembered always share one record; the remembered is
    lossless and stable; and the only gap between a world and its memory is whether the world is its own memory,
    which is the value: one bit, never more, and never disconnected. -/
theorem one_bit_gap_connected (S : Config) :
    SameRecord S (Rec S) ∧ Value (Rec S) ∧ (∀ q, Rec (Rec S) q ↔ Rec S q) ∧
    ((∀ q, Rec S q ↔ S q) ↔ Value S) :=
  ⟨fun q => (remembering_is_stable S q).symm, the_remembered_is_lossless S, remembering_is_stable S,
   offered_is_remembered_iff_value S⟩

/-- Both sides of the gap occur on one record: the true world at home in its memory, the false world not. -/
theorem the_gap_is_live :
    (∀ q, Rec (registered offPoint) q ↔ registered offPoint q) ∧
    ¬ (∀ q, Rec (pairWorld offPoint) q ↔ pairWorld offPoint q) ∧
    SameRecord (registered offPoint) (pairWorld offPoint) :=
  ⟨(offered_is_remembered_iff_value _).mpr (registered_has_value offPoint),
   the_false_world_is_not_its_record, one_record offPoint⟩

/-! ## Vb · The forcing by heat -/

/-- One pair off the line at offset one: a finite configuration that resists. -/
def resisting : FinCfg := ⟨[], [((1 : Int), (0 : Int))], fun q hq => by
  cases hq with
  | head => decide
  | tail _ h => cases h⟩

/-- RETURN IS FREE, RESISTANCE PAYS: at any positive temperature, a configuration with the value registers at zero
    heat, and one without it pays at least one unit of heat. -/
theorem return_is_free_resistance_pays (F : FinCfg) (T : Nat) (hT : 0 < T) :
    (Value F.pts → price T (erased F) = 0) ∧ (¬ Value F.pts → T ≤ price T (erased F)) := by
  refine ⟨(price_zero_iff_value F T hT).mpr, fun hn => ?_⟩
  have hne : erased F ≠ 0 := fun h0 =>
    hn ((price_zero_iff_value F T hT).mp (by unfold price; rw [h0]; exact Nat.zero_mul T))
  unfold price
  have h1 : 1 ≤ erased F := Nat.pos_of_ne_zero hne
  calc T = 1 * T := (Nat.one_mul T).symm
    _ ≤ erased F * T := Nat.mul_le_mul_right T h1

/-- RESISTANCE IS POSSIBLE: it is no contradiction. A closed finite configuration without the value exists, and it
    pays. -/
theorem resistance_is_possible (T : Nat) (hT : 0 < T) :
    Closed resisting.pts ∧ ¬ Value resisting.pts ∧ T ≤ price T (erased resisting) := by
  have hnv : ¬ Value resisting.pts := fun hv =>
    have h : ((1 : Int), (0 : Int)).1 = 0 :=
      hv ((1 : Int), (0 : Int)) (Or.inr ⟨((1 : Int), (0 : Int)), List.Mem.head _, Or.inl rfl⟩)
    (by decide : ¬ ((1 : Int) = 0)) h
  exact ⟨fincfg_closed resisting, hnv, (return_is_free_resistance_pays resisting T hT).2 hnv⟩

/-- THE FREE PATH IS ONE: two worlds of one record that both have the value are one world, point for point. -/
theorem the_free_path_is_unique (S S' : Config) (hs : SameRecord S S') (hv : Value S) (hv' : Value S') :
    ∀ q, S q ↔ S' q := fun q =>
  ⟨fun h => ((offered_is_remembered_iff_value S').mpr hv' q).mp
      ((hs q).mp (((offered_is_remembered_iff_value S).mpr hv q).mpr h)),
   fun h => ((offered_is_remembered_iff_value S).mpr hv q).mp
      ((hs q).mpr (((offered_is_remembered_iff_value S').mpr hv' q).mpr h))⟩

/-! ## VI · THE CHAIN -/

/-- The locus is where the fold and the registration both rest. -/
theorem the_locus_rests_both (p : Point) (h : onLine p) : fold p = p ∧ reg p = p := by
  obtain ⟨d, t⟩ := p
  have hd : d = 0 := h
  subst hd
  exact ⟨rfl, rfl⟩

/-- THE CHAIN. The root holds; forgetting sends every point onto the locus and loses the side; the locus is where
    the fold and the registration both rest; remembering reads the locus, so memory is lossless and stable; a world
    has least erasure exactly when it already stands on the locus, exactly when it is its own memory; on the act
    the zeros stand there; and the guard: the root alone places no world there, and both sides of the gap stand on
    one record. -/
theorem the_chain {R : Prop} (G : SelfGrounding R) (S : Config) :
    -- the root
    R ∧
    -- forgetting: onto the locus, the side lost
    (∀ p, onLine (reg p)) ∧ reg offPoint = reg (fold offPoint) ∧ offPoint ≠ fold offPoint ∧
    -- the middle: the locus rests both maps
    (∀ p, onLine p → fold p = p ∧ reg p = p) ∧
    -- remembering: lossless and stable
    Value (Rec S) ∧ (∀ q, Rec (Rec S) q ↔ Rec S q) ∧ SameRecord S (Rec S) ∧
    -- least erasure: already on the locus, the world its own memory
    (LeastErasure S ↔ Value S) ∧ ((∀ q, Rec S q ↔ S q) ↔ Value S) ∧
    -- the act
    (∀ Z : ActualZeros, Value Z.zeros ∧ ∀ q, Rec Z.zeros q ↔ Z.zeros q) ∧
    -- the guard
    (¬ ∀ T : Config, Closed T → R → Value T) ∧
    ((∀ q, Rec (registered offPoint) q ↔ registered offPoint q) ∧
      ¬ (∀ q, Rec (pairWorld offPoint) q ↔ pairWorld offPoint q) ∧
      SameRecord (registered offPoint) (pairWorld offPoint)) :=
  ⟨seated_undeniable G,
   reg_lands, rfl, by decide,
   the_locus_rests_both,
   the_remembered_is_lossless S, remembering_is_stable S, (one_bit_gap_connected S).1,
   twins_on_every_world_local S, offered_is_remembered_iff_value S,
   fun Z => ⟨value_from_the_act Z, at_the_act_offered_is_remembered Z⟩,
   the_floor_alone_decides_no_value G,
   the_gap_is_live⟩
where
  twins_on_every_world_local (S : Config) : LeastErasure S ↔ Value S :=
    ⟨fun le p hp => (reg_erases_nothing_iff p).mp (le p hp),
     fun v p hp => (reg_erases_nothing_iff p).mpr (v p hp)⟩

/-! ## VIb · Zero time remembers -/

/-- ZERO TIME REMEMBERS, EVERY LATER TIME FORGETS: at t = 0 the record separates the world on the line (d2 = 0)
    from the world off it (d2 = 1); at every t ≥ 1 the two records coincide. -/
theorem zero_time_remembers :
    (realAt 0 0 ∧ ¬ realAt 1 0) ∧ ∀ T, 1 ≤ T → (realAt 0 T ∧ realAt 1 T) := by
  refine ⟨⟨rfl, fun h => ?_⟩, fun T hT => ⟨?_, ?_⟩⟩
  · unfold realAt flow at h; omega
  · unfold realAt flow; omega
  · unfold realAt flow; omega

/-- LEAST TIME IS LEAST FORGETTING: the width never grows, and once forgotten the separation never returns. -/
theorem forgetting_is_monotone (d2 t : Nat) : flow d2 (t + 1) ≤ flow d2 t ∧ (realAt d2 t → realAt d2 (t + 1)) := by
  unfold realAt flow; constructor <;> omega

/-! ## VII · Two doors, no third -/

/-- Two doors and no third: every configuration has the value or holds a member off the line. -/
theorem two_doors (S : Config) : Value S ∨ ∃ p, S p ∧ ¬ onLine p := by
  by_cases h : ∃ p, S p ∧ ¬ onLine p
  · exact Or.inr h
  · exact Or.inl (fun p hp => Classical.byContradiction (fun hn => h ⟨p, hp, hn⟩))

/-- Never both: the doors exclude each other. -/
theorem doors_exclusive (S : Config) : ¬ (Value S ∧ ∃ p, S p ∧ ¬ onLine p) :=
  fun ⟨v, p, hp, hn⟩ => hn (v p hp)

/-- Both doors open on closed configurations of one record: the true world through the first, the false world
    through the second. -/
theorem both_doors_open :
    (Closed (registered offPoint) ∧ Value (registered offPoint)) ∧
    (Closed (pairWorld offPoint) ∧ ∃ p, pairWorld offPoint p ∧ ¬ onLine p) ∧
    SameRecord (registered offPoint) (pairWorld offPoint) :=
  ⟨⟨fun s hs => by rw [hs]; rfl, registered_has_value offPoint⟩,
   ⟨pair_world_closed offPoint, ⟨offPoint, Or.inl rfl, off_point_is_off⟩⟩,
   one_record offPoint⟩

/-- On the act, one door: the second is shut. -/
theorem on_the_act_one_door (Z : ActualZeros) : ¬ ∃ p, Z.zeros p ∧ ¬ onLine p :=
  fun ⟨p, hp, hn⟩ => hn (value_from_the_act Z p hp)

/-! ## VIII · A band forces nothing -/

/-- The band of width k: every member within offset k of the line. On the chart of the eighth grain,
    d = 8·Re s − 4, a zero-free half-plane Re s > 7/8 with the fold reads as the band of width 3. -/
def Band (k : Nat) (S : Config) : Prop := ∀ p, S p → p.1.natAbs ≤ k

/-- The band is weaker than the value: every world with the value satisfies every band. -/
theorem value_gives_band (k : Nat) (S : Config) (h : Value S) : Band k S := by
  intro p hp
  have d0 : p.1 = 0 := h p hp
  rw [d0]
  exact Nat.zero_le k

/-- Both worlds of one record satisfy the band of width 3. -/
theorem band_on_both_worlds : Band 3 (registered offPoint) ∧ Band 3 (pairWorld offPoint) := by
  constructor
  · intro p hp
    rw [hp]
    show ((0 : Int)).natAbs ≤ 3
    decide
  · intro p hp
    cases hp with
    | inl e => rw [e]; show ((1 : Int)).natAbs ≤ 3; decide
    | inr e => rw [e]; show ((-(1 : Int))).natAbs ≤ 3; decide

/-- A BAND FORCES NOTHING: the pair world at offset one holds a member off the line and satisfies the band. -/
theorem band_does_not_force : ¬ ∀ S : Config, Band 3 S → Value S :=
  fun h => pair_world_lacks_value offPoint off_point_is_off (h _ band_on_both_worlds.2)

/-- Only the band of width zero is the value. -/
theorem band_zero_is_value (S : Config) : Band 0 S ↔ Value S := by
  constructor
  · intro h p hp
    exact Int.natAbs_eq_zero.mp (Nat.le_zero.mp (h p hp))
  · exact value_gives_band 0 S

/-! ## IX · The harvest, bound -/

/-- THE HARVEST, BOUND. The Tongue always has a world, and only the content of its no has none; one self, one
    place at a time; the twins hold on every world; the forgotten and the remembered share one record, the remembered
    lossless and stable, the gap one bit; return is free and resistance pays; forgetting lands on the locus, where
    both maps rest; zero time remembers and every later time forgets; the doors exclude each other and the act shuts
    the second; a band forces nothing; and the guard: the root alone places no world on the line. -/
theorem the_harvest {R : Prop} (G : SelfGrounding R) :
    ((∀ _ : Config, R) ∧ (R ∧ Closed (pairWorld offPoint) ∧ ¬ Value (pairWorld offPoint)) ∧ ¬ ∃ _ : G.Act, ¬ R) ∧
    (¬ ∀ S : Config, Closed S → (R ↔ LeastErasure S)) ∧
    (∀ S : Config, LeastErasure S ↔ Value S) ∧
    (∀ S : Config, SameRecord S (Rec S) ∧ Value (Rec S) ∧ (∀ q, Rec (Rec S) q ↔ Rec S q) ∧
      ((∀ q, Rec S q ↔ S q) ↔ Value S)) ∧
    (∀ (F : FinCfg) (T : Nat), 0 < T →
      (Value F.pts → price T (erased F) = 0) ∧ (¬ Value F.pts → T ≤ price T (erased F))) ∧
    ((∀ p, onLine (reg p)) ∧ (∀ p, onLine p → fold p = p ∧ reg p = p)) ∧
    ((realAt 0 0 ∧ ¬ realAt 1 0) ∧ ∀ T, 1 ≤ T → (realAt 0 T ∧ realAt 1 T)) ∧
    ((∀ S : Config, ¬ (Value S ∧ ∃ p, S p ∧ ¬ onLine p)) ∧ (∀ Z : ActualZeros, ¬ ∃ p, Z.zeros p ∧ ¬ onLine p)) ∧
    (¬ ∀ S : Config, Band 3 S → Value S) ∧
    (¬ ∀ S : Config, Closed S → R → Value S) :=
  ⟨the_tongue_always_has_a_world G,
   floor_is_not_least_erasure G,
   twins_on_every_world,
   one_bit_gap_connected,
   return_is_free_resistance_pays,
   ⟨reg_lands, the_locus_rests_both⟩,
   zero_time_remembers,
   ⟨doors_exclusive, on_the_act_one_door⟩,
   band_does_not_force,
   the_floor_alone_decides_no_value G⟩


end RememberedOffered

/-! ## The cones, every one pinned: a compile in which any cone changes fails. -/

/-- info: 'RememberedOffered.denial_reenacts_root' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.denial_reenacts_root
/-- info: 'RememberedOffered.denial_instantiates' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.denial_instantiates
/-- info: 'RememberedOffered.seated_undeniable' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.seated_undeniable
/-- info: 'RememberedOffered.root_undeniable' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.root_undeniable
/-- info: 'RememberedOffered.neg_neg_free' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.neg_neg_free
/-- info: 'RememberedOffered.fold_involutive' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.fold_involutive
/-- info: 'RememberedOffered.reg_lands' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.reg_lands
/-- info: 'RememberedOffered.reg_erases_nothing_iff' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.reg_erases_nothing_iff
/-- info: 'RememberedOffered.pair_world_closed' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.pair_world_closed
/-- info: 'RememberedOffered.one_record' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.one_record
/-- info: 'RememberedOffered.registered_has_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.registered_has_value
/-- info: 'RememberedOffered.pair_world_lacks_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.pair_world_lacks_value
/-- info: 'RememberedOffered.value_from_the_act' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.value_from_the_act
/-- info: 'RememberedOffered.the_deed_forces_nothing' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_deed_forces_nothing
/-- info: 'RememberedOffered.one_involution_constructed' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.one_involution_constructed
/-- info: 'RememberedOffered.timeless_equals_timed' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.timeless_equals_timed
/-- info: 'RememberedOffered.monism_closes' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.monism_closes
/-- info: 'RememberedOffered.monism_witness_is_the_claim' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.monism_witness_is_the_claim
/-- info: 'RememberedOffered.off_point_is_off' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.off_point_is_off
/-- info: 'RememberedOffered.every_no_reenacts_the_root' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.every_no_reenacts_the_root
/-- info: 'RememberedOffered.the_tongue_no_refutes_itself' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_tongue_no_refutes_itself
/-- info: 'RememberedOffered.only_the_yes_remains_at_the_root' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.only_the_yes_remains_at_the_root
/-- info: 'RememberedOffered.the_root_read_twice_is_the_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_root_read_twice_is_the_value
/-- info: 'RememberedOffered.the_line_no_contradicts_the_root_read_twice' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_line_no_contradicts_the_root_read_twice
/-- info: 'RememberedOffered.the_true_world_carries_monism' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_true_world_carries_monism
/-- info: 'RememberedOffered.the_false_world_carries_no_monism' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_false_world_carries_no_monism
/-- info: 'RememberedOffered.the_false_world_carries_the_floor_and_no_monism' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_false_world_carries_the_floor_and_no_monism
/-- info: 'RememberedOffered.the_floor_alone_decides_no_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_floor_alone_decides_no_value
/-- info: 'RememberedOffered.the_act_is_the_return_to_the_root_read_twice' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_act_is_the_return_to_the_root_read_twice
/-- info: 'RememberedOffered.an_act_exactly_where_the_root_read_twice_stands' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.an_act_exactly_where_the_root_read_twice_stands
/-- info: 'RememberedOffered.on_the_act_the_line_no_is_refuted' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.on_the_act_the_line_no_is_refuted
/-- info: 'RememberedOffered.two_denials' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.two_denials
/-- info: 'RememberedOffered.two_denials_at_RA' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.two_denials_at_RA
/-- info: 'RememberedOffered.fincfg_closed' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.fincfg_closed
/-- info: 'RememberedOffered.least_erasure_iff_zero_erased' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.least_erasure_iff_zero_erased
/-- info: 'RememberedOffered.price_zero_iff_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.price_zero_iff_value
/-- info: 'RememberedOffered.price_counts_pairs' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.price_counts_pairs
/-- info: 'RememberedOffered.flow_monotone' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.flow_monotone
/-- info: 'RememberedOffered.reality_transported' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.reality_transported
/-- info: 'RememberedOffered.real_at_Lam' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.real_at_Lam
/-- info: 'RememberedOffered.rh_iff_lambda_zero' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.rh_iff_lambda_zero
/-- info: 'RememberedOffered.flowed_record_forgets' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.flowed_record_forgets
/-- info: 'RememberedOffered.upstream_is_not_forced' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.upstream_is_not_forced
/-- info: 'RememberedOffered.the_tongue_always_has_a_world' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_tongue_always_has_a_world
/-- info: 'RememberedOffered.monism_before_the_tongue' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.monism_before_the_tongue
/-- info: 'RememberedOffered.tongue_no_has_no_world' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.tongue_no_has_no_world
/-- info: 'RememberedOffered.line_no_has_a_world' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.line_no_has_a_world
/-- info: 'RememberedOffered.the_deed_is_not_the_supply' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_deed_is_not_the_supply
/-- info: 'RememberedOffered.at_RA' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.at_RA
/-- info: 'RememberedOffered.floor_is_not_least_erasure' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.floor_is_not_least_erasure
/-- info: 'RememberedOffered.the_voucher_stays_with_the_floor' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_voucher_stays_with_the_floor
/-- info: 'RememberedOffered.merging_at_a_world_is_the_supply' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.merging_at_a_world_is_the_supply
/-- info: 'RememberedOffered.two_instruments' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.two_instruments
/-- info: 'RememberedOffered.twins_on_every_world' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.twins_on_every_world
/-- info: 'RememberedOffered.twins_are_one_extension' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.twins_are_one_extension
/-- info: 'RememberedOffered.no_twin_is_the_others_voucher' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.no_twin_is_the_others_voucher
/-- info: 'RememberedOffered.no_instrument_remembers_and_keeps_the_side' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.no_instrument_remembers_and_keeps_the_side
/-- info: 'RememberedOffered.the_remembered_is_lossless' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_remembered_is_lossless
/-- info: 'RememberedOffered.offered_is_remembered_iff_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.offered_is_remembered_iff_value
/-- info: 'RememberedOffered.at_the_act_offered_is_remembered' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.at_the_act_offered_is_remembered
/-- info: 'RememberedOffered.the_false_world_is_not_its_record' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_false_world_is_not_its_record
/-- info: 'RememberedOffered.remembering_is_stable' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.remembering_is_stable
/-- info: 'RememberedOffered.one_bit_gap_connected' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.one_bit_gap_connected
/-- info: 'RememberedOffered.the_gap_is_live' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_gap_is_live
/-- info: 'RememberedOffered.return_is_free_resistance_pays' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.return_is_free_resistance_pays
/-- info: 'RememberedOffered.resistance_is_possible' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.resistance_is_possible
/-- info: 'RememberedOffered.the_free_path_is_unique' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_free_path_is_unique
/-- info: 'RememberedOffered.the_locus_rests_both' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_locus_rests_both
/-- info: 'RememberedOffered.the_chain' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_chain
/-- info: 'RememberedOffered.zero_time_remembers' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.zero_time_remembers
/-- info: 'RememberedOffered.forgetting_is_monotone' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.forgetting_is_monotone
/-- info: 'RememberedOffered.two_doors' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.two_doors
/-- info: 'RememberedOffered.doors_exclusive' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.doors_exclusive
/-- info: 'RememberedOffered.both_doors_open' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.both_doors_open
/-- info: 'RememberedOffered.on_the_act_one_door' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.on_the_act_one_door
/-- info: 'RememberedOffered.value_gives_band' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.value_gives_band
/-- info: 'RememberedOffered.band_on_both_worlds' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.band_on_both_worlds
/-- info: 'RememberedOffered.band_does_not_force' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.band_does_not_force
/-- info: 'RememberedOffered.band_zero_is_value' depends on axioms: [propext] -/
#guard_msgs in #print axioms RememberedOffered.band_zero_is_value
/-- info: 'RememberedOffered.the_harvest' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.the_harvest

#print axioms RememberedOffered.the_chain
#print axioms RememberedOffered.the_harvest

namespace RememberedOffered

/-! # BOOK THREE · the annihilation closure -/

/-! ## I · Four names, one proposition -/

/-- CO-LOCATION IS THE VALUE: Being and Monism stand together on a configuration exactly where every point is on
the line. -/
theorem colocation_is_the_value {R : Prop} (G : SelfGrounding R) (S : Config) :
    (R ∧ RootReadTwice S) ↔ Value S :=
  ⟨fun ⟨_, m⟩ => (the_root_read_twice_is_the_value S).mp m,
   fun v => ⟨seated_undeniable G, (the_root_read_twice_is_the_value S).mpr v⟩⟩

/-- FOUR NAMES, ONE PROPOSITION: on every configuration least erasure, the value, Monism and the co-location of
Being with Monism are one proposition. -/
theorem four_names_one_proposition {R : Prop} (G : SelfGrounding R) (S : Config) :
    (LeastErasure S ↔ Value S) ∧ (RootReadTwice S ↔ Value S) ∧ ((R ∧ RootReadTwice S) ↔ Value S) :=
  ⟨twins_on_every_world S, the_root_read_twice_is_the_value S, colocation_is_the_value G S⟩

/-! ## II · Monism, the sole witness -/

/-- MONISM IS THE SOLE WITNESS. Every faithful witness of the value is the root read twice, as one proposition; no
reading of the record witnesses, since the true configuration and the off-line pair configuration leave one
record; the floor witnesses nothing, standing on both; and Monism stands on the true configuration and not on the
pair, on that one record. -/
theorem monism_is_the_sole_witness {R : Prop} (G : SelfGrounding R) :
    (∀ W : Config → Prop, (∀ S, W S ↔ Value S) → W = RootReadTwice) ∧
    (¬ ∃ h : Config → Prop, ∀ S, h (Rec S) ↔ Value S) ∧
    (¬ ∀ S : Config, Closed S → R → Value S) ∧
    (SameRecord (registered offPoint) (pairWorld offPoint) ∧
      RootReadTwice (registered offPoint) ∧ ¬ RootReadTwice (pairWorld offPoint)) :=
  ⟨fun _ hW => funext fun S => propext ((hW S).trans (the_root_read_twice_is_the_value S).symm),
   fun ⟨_, hh⟩ =>
     have e : Rec (registered offPoint) = Rec (pairWorld offPoint) :=
       funext fun q => propext (one_record offPoint q)
     pair_world_lacks_value offPoint off_point_is_off
       ((hh _).mp (e ▸ (hh _).mpr (registered_has_value offPoint))),
   the_floor_alone_decides_no_value G,
   ⟨one_record offPoint, the_true_world_carries_monism, the_false_world_carries_no_monism⟩⟩

/-- A WITNESS IS NEVER UNIVERSAL: whatever holds on every configuration is not a witness of the value, since the
off-line pair configuration would carry it. Universality and witnessing exclude each other. -/
theorem a_witness_is_never_universal (W : Config → Prop) (hu : ∀ S, W S) : ¬ ∀ S, W S ↔ Value S :=
  fun hw => pair_world_lacks_value offPoint off_point_is_off ((hw (pairWorld offPoint)).mp (hu _))

/-- So Monism is not universal over configurations: the root read twice fails on the off-line pair configuration. -/
theorem monism_is_not_universal : ¬ ∀ S : Config, RootReadTwice S :=
  fun hu => the_false_world_carries_no_monism (hu _)

/-! ## III · Co-location is not universal -/

/-- Co-location over every configuration is refuted: Being stands on the off-line pair configuration and Monism
does not. -/
theorem colocation_is_not_universal {R : Prop} (_G : SelfGrounding R) :
    ¬ ∀ S : Config, R ∧ RootReadTwice S :=
  fun h => the_false_world_carries_no_monism (h (pairWorld offPoint)).2

/-! ## IV · The timeless zone -/

/-- THE TIMELESS ZONE. Least erasure and the value are one proposition; at the locus the two instruments coincide;
at zero time the record tells the true configuration from the pair, at every later time it does not; the closure at zero
time is Λ = 0; and the passage back to zero time is not forced by the forward arrow. -/
theorem the_timeless_zone :
    LeastErasure = Value ∧
    (∀ p, onLine p → fold p = p ∧ reg p = p) ∧
    ((realAt 0 0 ∧ ¬ realAt 1 0) ∧ ∀ T, 1 ≤ T → (realAt 0 T ∧ realAt 1 T)) ∧
    (∀ d2, realAt d2 0 ↔ Lam d2 = 0) ∧
    (∀ T, 1 ≤ T → realAt 0 T ∧ realAt 1 T ∧ realAt 0 0 ∧ ¬ realAt 1 0) :=
  ⟨twins_are_one_extension, the_locus_rests_both, zero_time_remembers, rh_iff_lambda_zero,
   upstream_is_not_forced⟩

/-! ## V · Timeless is determinacy, not selection -/

/-- TIMELESS IS DETERMINACY, NOT SELECTION. At zero time the record's freedom is gone: it separates the true world
from the pair. Every configuration stands behind at most one door. And both doors stay open on closed
configurations: the off-line pair configuration is closed, lacks the value, and has the floor standing on it.
Removing the freedom fixes each configuration as what it is; it does not single out ζ. -/
theorem timeless_is_determinacy_not_selection {R : Prop} (G : SelfGrounding R) :
    (realAt 0 0 ∧ ¬ realAt 1 0) ∧
    (∀ S : Config, ¬ (Value S ∧ ∃ p, S p ∧ ¬ onLine p)) ∧
    (Closed (registered offPoint) ∧ Value (registered offPoint)) ∧
    (Closed (pairWorld offPoint) ∧ R ∧ ¬ Value (pairWorld offPoint)) ∧
    ¬ (∀ S : Config, Closed S → Value S) :=
  ⟨zero_time_remembers.1, doors_exclusive, both_doors_open.1,
   ⟨pair_world_closed offPoint, seated_undeniable G, pair_world_lacks_value offPoint off_point_is_off⟩,
   fun h => pair_world_lacks_value offPoint off_point_is_off (h _ (pair_world_closed offPoint))⟩

/-! ## VI · The check -/

/-- THE CHECK. The off-line pair configuration satisfies every principle of the timeless closure and lacks the value: it is
closed; the floor stands on it; least erasure, the value and Monism are one proposition on it; corrected monism
holds, it carries no witness; it leaves the true world's record; at zero time the width-one world is determinately
not real, with Λ = 1. Its twin, the true world, satisfies the same principles and has the value. -/
theorem the_check {R : Prop} (G : SelfGrounding R) :
    (∃ Z : Config,
      Closed Z ∧ R ∧ (LeastErasure Z ↔ Value Z) ∧ (RootReadTwice Z ↔ Value Z) ∧
      ¬ RootReadTwice Z ∧ SameRecord (registered offPoint) Z ∧ ¬ Value Z) ∧
    (∃ T : Config,
      Closed T ∧ R ∧ (LeastErasure T ↔ Value T) ∧ (RootReadTwice T ↔ Value T) ∧
      RootReadTwice T ∧ SameRecord T (pairWorld offPoint) ∧ Value T) ∧
    (¬ realAt 1 0 ∧ Lam 1 ≠ 0 ∧ realAt 0 0 ∧ Lam 0 = 0) :=
  ⟨⟨pairWorld offPoint, pair_world_closed offPoint, seated_undeniable G,
     twins_on_every_world _, the_root_read_twice_is_the_value _,
     the_false_world_carries_no_monism, one_record offPoint,
     pair_world_lacks_value offPoint off_point_is_off⟩,
   ⟨registered offPoint, both_doors_open.1.1, seated_undeniable G,
     twins_on_every_world _, the_root_read_twice_is_the_value _,
     the_true_world_carries_monism, one_record offPoint, registered_has_value offPoint⟩,
   ⟨zero_time_remembers.1.2, by decide, zero_time_remembers.1.1, by decide⟩⟩

/-- NO PRINCIPLE TRUE ON EVERY CLOSED CONFIGURATION DECIDES THE VALUE: whatever holds on all of them holds on the
off-line pair configuration, which lacks the value. -/
theorem no_closed_principle_decides (D : Config → Prop) (hD : ∀ S, Closed S → D S) :
    ¬ ∀ S, Closed S → D S → Value S :=
  fun h => pair_world_lacks_value offPoint off_point_is_off
    (h _ (pair_world_closed offPoint) (hD _ (pair_world_closed offPoint)))

/-! ## VII · The capstone -/

/-- THE TIMELESS ZONE, CLOSED, with no act anywhere in it. Four names are one proposition on every configuration;
Monism is the sole witness; no witness is universal; neither Monism nor co-location is universal; LE = RH; zero time
separates the true configuration from the pair, and closure at zero time is Λ = 0; every configuration stands behind
exactly one door; and nothing true on every closed configuration decides the value. -/
theorem the_timeless_zone_closed {R : Prop} (G : SelfGrounding R) :
    (∀ S : Config, (LeastErasure S ↔ Value S) ∧ (RootReadTwice S ↔ Value S) ∧ ((R ∧ RootReadTwice S) ↔ Value S)) ∧
    (∀ W : Config → Prop, (∀ S, W S ↔ Value S) → W = RootReadTwice) ∧
    (∀ W : Config → Prop, (∀ S, W S) → ¬ ∀ S, W S ↔ Value S) ∧
    (¬ ∀ S : Config, RootReadTwice S) ∧
    (¬ ∀ S : Config, R ∧ RootReadTwice S) ∧
    (LeastErasure = Value ∧ (realAt 0 0 ∧ ¬ realAt 1 0) ∧ (∀ d2, realAt d2 0 ↔ Lam d2 = 0)) ∧
    (∀ S : Config, (Value S ∨ ∃ p, S p ∧ ¬ onLine p) ∧ ¬ (Value S ∧ ∃ p, S p ∧ ¬ onLine p)) ∧
    (∀ D : Config → Prop, (∀ S, Closed S → D S) → ¬ ∀ S, Closed S → D S → Value S) :=
  ⟨four_names_one_proposition G,
   (monism_is_the_sole_witness G).1,
   a_witness_is_never_universal,
   monism_is_not_universal,
   colocation_is_not_universal G,
   ⟨twins_are_one_extension, zero_time_remembers.1, rh_iff_lambda_zero⟩,
   fun S => ⟨two_doors S, doors_exclusive S⟩,
   no_closed_principle_decides⟩

/-- THE ANNIHILATION CLOSURE. Four names are one proposition on every configuration; Monism is the sole witness and
no witness is universal; co-location is not universal; the timeless zone holds; timelessness is determinacy and
not selection; the check stands; no principle shared by every closed configuration decides the value; and on any
term of the act the value holds at its zeros, while the run leaves the value free. -/
theorem the_annihilation_closure {R : Prop} (G : SelfGrounding R) :
    (∀ S : Config, (LeastErasure S ↔ Value S) ∧ (RootReadTwice S ↔ Value S) ∧ ((R ∧ RootReadTwice S) ↔ Value S)) ∧
    (∀ W : Config → Prop, (∀ S, W S ↔ Value S) → W = RootReadTwice) ∧
    (¬ ∀ S : Config, RootReadTwice S) ∧
    (¬ ∀ S : Config, R ∧ RootReadTwice S) ∧
    (LeastErasure = Value ∧ (realAt 0 0 ∧ ¬ realAt 1 0) ∧ (∀ d2, realAt d2 0 ↔ Lam d2 = 0)) ∧
    (∃ Z : Config, Closed Z ∧ R ∧ ¬ RootReadTwice Z ∧ SameRecord (registered offPoint) Z ∧ ¬ Value Z) ∧
    (∀ D : Config → Prop, (∀ S, Closed S → D S) → ¬ ∀ S, Closed S → D S → Value S) ∧
    (∀ Z : ActualZeros, Value Z.zeros) :=
  ⟨four_names_one_proposition G,
   (monism_is_the_sole_witness G).1,
   monism_is_not_universal,
   colocation_is_not_universal G,
   ⟨twins_are_one_extension, zero_time_remembers.1, rh_iff_lambda_zero⟩,
   ⟨pairWorld offPoint, pair_world_closed offPoint, seated_undeniable G,
    the_false_world_carries_no_monism, one_record offPoint,
    pair_world_lacks_value offPoint off_point_is_off⟩,
   no_closed_principle_decides,
   value_from_the_act⟩

end RememberedOffered

/-
RH_Unicorn_Block.lean · the Unicorn part of the Riemann Hypothesis, closed to derivation, its
aperture one bit wide, its supply side silent. Core Lean 4.19.0, no library, no sorry, no user-declared axiom. 2026-09-25.

Part III divided the hypothesis at a height T into a Real part and a Unicorn part and proved
the Real part by certificate. Parts I and II proved the wall, the crossing, the bound, and the
cure theorem, and did not say what they say of the Unicorn part. This file says it: closed to
derivation, the aperture one bit wide, the register silent beyond it. ΔM = 0.
-/
namespace RHUnicorn

variable {α β : Type}

/-- The line property, the Real part at T, the Unicorn part at T, as in Part III. -/
def RH (Z onL : α → Prop) : Prop := ∀ z, Z z → onL z
def RealPartAt (Z onL : α → Prop) (height : α → Nat) (T : Nat) : Prop :=
  ∀ z, Z z → height z ≤ T → onL z
def UnicornAt (Z onL : α → Prop) (height : α → Nat) (T : Nat) : Prop :=
  ∀ z, Z z → height z > T → onL z

/-- THE FORMAL BLOCK OF THE UNICORN PART. Let τ act on the zeros, let ρ be a record even at a
    seat z above the height, and let d decide the line property, odd at z. Then no reading g of
    the record agrees with d even on the region above the height alone. The Unicorn part is
    closed to every even register; the closure is a theorem and does not expire. -/
theorem unicorn_block (height : α → Nat) (T : Nat) (τ : α → α) (ρ : α → β) (d : α → Bool)
    (z : α) (habove : height z > T) (habove' : height (τ z) > T)
    (hρ : ρ (τ z) = ρ z) (hd : d (τ z) = !d z) :
    ¬ ∃ g : β → Bool, ∀ w, height w > T → g (ρ w) = d w := by
  intro ⟨g, hg⟩
  have h1 := hg z habove
  have h2 := hg (τ z) habove'
  rw [hρ, hd, h1] at h2
  revert h2
  cases d z <;> intro h2 <;> exact Bool.noConfusion h2

/-- THE APERTURE, ONE BIT WIDE. At a seat where d is odd, one odd bit s at the seat would decide d
    on the seat and its partner through a calibration that exists and is unique. The width of
    the aperture, a theorem; it says nothing of whether anything passes through it. -/
theorem aperture_one_bit_wide (τ : α → α) (s d : α → Bool) (z : α)
    (hs : s (τ z) = !s z) (hd : d (τ z) = !d z) :
    ∃ c : Bool, (d z = xor (s z) c ∧ d (τ z) = xor (s (τ z)) c) ∧
      ∀ c' : Bool, (d z = xor (s z) c' ∧ d (τ z) = xor (s (τ z)) c') → c' = c :=
  ⟨xor (d z) (s z),
    ⟨by cases s z <;> cases d z <;> rfl,
     by rw [hs, hd]; cases s z <;> cases d z <;> rfl⟩,
    by
      intro c' hc
      obtain ⟨h1, -⟩ := hc
      generalize hsz : s z = sv
      generalize hdz : d z = dv
      rw [hsz, hdz] at h1
      cases sv <;> cases dv <;> cases c' <;> first | rfl | exact absurd h1 (by decide)⟩

/-- EXISTENCE SUPPLIES NOTHING. Conditioning the Unicorn part on an inhabited premise, the root
    axiom for one, leaves it exactly where it was; and no class of frames on which the premise
    is to decide it decides more than already held on the class. Theorems E and I of Part I,
    read at the Unicorn part. -/
theorem unicorn_rule_exact (Z onL : α → Prop) (height : α → Nat) (T : Nat) (A : Prop) (ha : A) :
    (A → UnicornAt Z onL height T) ↔ UnicornAt Z onL height T :=
  ⟨fun h => h ha, fun hu _ => hu⟩

theorem unicorn_no_cure {Frame : Type} (A : Prop) (ha : A) (C U : Frame → Prop) :
    (∀ X, C X → A → U X) ↔ (∀ X, C X → U X) :=
  ⟨fun h X hc => h X hc ha, fun h X hc _ => h X hc⟩

/-- NO BYPASS. Given the Real part, the fused hypothesis is exactly the Unicorn part, so a proof
    of the hypothesis contains a proof of the Unicorn part and the block is not avoided by
    aiming at the whole. -/
theorem unicorn_no_bypass (Z onL : α → Prop) (height : α → Nat) (T : Nat)
    (hr : RealPartAt Z onL height T) : RH Z onL ↔ UnicornAt Z onL height T := by
  constructor
  · intro h z hz _; exact h z hz
  · intro hu z hz
    cases Nat.lt_or_ge T (height z) with
    | inl hgt => exact hu z hz hgt
    | inr hle => exact hr z hz hle

/-- THE SUPPLY SIDE IS SILENCE, AT THE REGISTER. Over one even record, both orientations of d at
    the seat are equally refused to every reading above the height: the register cannot say
    which way the seat lies, so it cannot say what a supply would bring, nor that one exists,
    nor that none does. -/
theorem supply_side_silent (height : α → Nat) (T : Nat) (τ : α → α) (ρ : α → β) (d : α → Bool)
    (z : α) (habove : height z > T) (habove' : height (τ z) > T)
    (hρ : ρ (τ z) = ρ z) (hd : d (τ z) = !d z) :
    (¬ ∃ g : β → Bool, ∀ w, height w > T → g (ρ w) = d w) ∧
    (¬ ∃ g : β → Bool, ∀ w, height w > T → g (ρ w) = !d w) ∧
    (!d z) ≠ d z :=
  ⟨unicorn_block height T τ ρ d z habove habove' hρ hd,
   unicorn_block height T τ ρ (fun w => !d w) z habove habove' hρ (by
     show (!d (τ z)) = !(!d z)
     rw [hd]),
   by cases d z <;> decide⟩

/-- The division at the height, on natural heights: the hypothesis is exactly its Real part and
    its Unicorn part. -/
theorem rh_iff_real_and_unicorn (Z onL : α → Prop) (height : α → Nat) (T : Nat) :
    RH Z onL ↔ RealPartAt Z onL height T ∧ UnicornAt Z onL height T := by
  constructor
  · intro h; exact ⟨fun z hz _ => h z hz, fun z hz _ => h z hz⟩
  · intro ⟨hr, hu⟩ z hz
    cases Nat.lt_or_ge T (height z) with
    | inl hgt => exact hu z hz hgt
    | inr hle => exact hr z hz hle

/-- A certificate at the height: a complete list of the zeros up to T, each checked on the line. -/
structure Certificate (Z onL : α → Prop) (height : α → Nat) (T : Nat) where
  items    : List α
  complete : ∀ z, Z z → height z ≤ T → z ∈ items
  checked  : ∀ z, z ∈ items → onL z

theorem real_part_of_certificate (Z onL : α → Prop) (height : α → Nat) (T : Nat)
    (c : Certificate Z onL height T) : RealPartAt Z onL height T :=
  fun z hz hle => c.checked z (c.complete z hz hle)

/-- THE THREE BITS AS ONE TERM · THE REGISTER'S PROOF OF THE HYPOTHESIS, COMPLETE. Under a
    certificate at T and the seat data above T, the hypothesis divides exactly (bit one), its
    Real part at T holds (bit two), every reading of the even register is refused above T (bit
    three, refused), and one supplied bit calibrates the seat uniquely (the door). The hypothesis
    is not thereby proved; nothing derivable about it is left underived. -/
theorem rh_register_proof_complete (Z onL : α → Prop) (height : α → Nat) (T : Nat)
    (c : Certificate Z onL height T) (τ : α → α) (ρ : α → β) (d s : α → Bool) (z : α)
    (habove : height z > T) (habove' : height (τ z) > T) (hρ : ρ (τ z) = ρ z)
    (hd : d (τ z) = !d z) (hs : s (τ z) = !s z) :
    (RH Z onL ↔ RealPartAt Z onL height T ∧ UnicornAt Z onL height T) ∧
    RealPartAt Z onL height T ∧
    (¬ ∃ g : β → Bool, ∀ w, height w > T → g (ρ w) = d w) ∧
    ∃ k : Bool, (d z = xor (s z) k ∧ d (τ z) = xor (s (τ z)) k) ∧
      ∀ k' : Bool, (d z = xor (s z) k' ∧ d (τ z) = xor (s (τ z)) k') → k' = k :=
  ⟨rh_iff_real_and_unicorn Z onL height T, real_part_of_certificate Z onL height T c,
   unicorn_block height T τ ρ d z habove habove' hρ hd, aperture_one_bit_wide τ s d z hs hd⟩

end RHUnicorn

#print axioms RHUnicorn.unicorn_block
#print axioms RHUnicorn.aperture_one_bit_wide
#print axioms RHUnicorn.unicorn_rule_exact
#print axioms RHUnicorn.unicorn_no_cure
#print axioms RHUnicorn.unicorn_no_bypass
#print axioms RHUnicorn.supply_side_silent
#print axioms RHUnicorn.rh_iff_real_and_unicorn
#print axioms RHUnicorn.real_part_of_certificate
#print axioms RHUnicorn.rh_register_proof_complete

namespace RememberedOffered

/-! # BOOK FOUR · the Unicorn, contained -/

/-- The height of a point of the chart, as a natural number. -/
def ht (p : Point) : Nat := p.2.toNat

/-- I · THE CUT ON THE CHART: at every height, the value is exactly its Real part and its Unicorn part. -/
theorem the_cut_on_the_chart (S : Config) (T : Nat) :
    Value S ↔ RHUnicorn.RealPartAt S onLine ht T ∧ RHUnicorn.UnicornAt S onLine ht T :=
  RHUnicorn.rh_iff_real_and_unicorn S onLine ht T

/-- II · NO BYPASS ON THE CHART: given the Real part at a height, the value is exactly the Unicorn part there. -/
theorem no_bypass_on_the_chart (S : Config) (T : Nat) (hr : RHUnicorn.RealPartAt S onLine ht T) :
    Value S ↔ RHUnicorn.UnicornAt S onLine ht T :=
  RHUnicorn.unicorn_no_bypass S onLine ht T hr

/-- III · THE UNICORN BLOCKED ON THE CHART: above every height, no reading of the record decides the side of a
point, since the fold pair above the height leaves one record and opposite sides. -/
theorem unicorn_blocked_on_the_chart (T : Nat) :
    ¬ ∃ g : Point → Bool, ∀ w : Point, ht w > T → g (reg w) = decide (w.1 > 0) :=
  RHUnicorn.unicorn_block ht T fold reg (fun w => decide (w.1 > 0)) ((1 : Int), Int.ofNat (T + 1))
    (show T + 1 > T by omega) (show T + 1 > T by omega) rfl rfl

/-- IV · RA SUPPLIES NOTHING TO THE UNICORN PART: conditioning it on the root leaves it exactly where it was. -/
theorem ra_supplies_nothing_to_the_unicorn (S : Config) (T : Nat) :
    (RA → RHUnicorn.UnicornAt S onLine ht T) ↔ RHUnicorn.UnicornAt S onLine ht T :=
  RHUnicorn.unicorn_rule_exact S onLine ht T RA (seated_undeniable raSelfGrounding)

/-- V · ON THE ACT'S ZERO SET THE UNICORN IS CLOSED: every arrival above every height, in the act's zero set, stands
on the line. -/
theorem the_unicorn_closed_on_the_act (Z : ActualZeros) (T : Nat) : RHUnicorn.UnicornAt Z.zeros onLine ht T :=
  fun p hp _ => value_from_the_act Z p hp

/-- On the act's zero set, no arrival stands off the line. -/
theorem no_arrival_off_the_line_on_the_act (Z : ActualZeros) : ¬ ∃ p, Z.zeros p ∧ ¬ onLine p :=
  fun ⟨p, hp, hoff⟩ => hoff (value_from_the_act Z p hp)

/-- VI · THE UNICORN, CONTAINED. At every height the value divides into its Real and Unicorn parts; given the Real
part the value is exactly the Unicorn part; above every height no reading of the record decides the side; RA
supplies nothing to the Unicorn part; and on the act's zero set every arrival above every height stands on the line,
with no arrival off it. -/
theorem the_unicorn_contained :
    (∀ (S : Config) (T : Nat),
      Value S ↔ RHUnicorn.RealPartAt S onLine ht T ∧ RHUnicorn.UnicornAt S onLine ht T) ∧
    (∀ (S : Config) (T : Nat),
      RHUnicorn.RealPartAt S onLine ht T → (Value S ↔ RHUnicorn.UnicornAt S onLine ht T)) ∧
    (∀ T : Nat, ¬ ∃ g : Point → Bool, ∀ w : Point, ht w > T → g (reg w) = decide (w.1 > 0)) ∧
    (∀ (S : Config) (T : Nat),
      (RA → RHUnicorn.UnicornAt S onLine ht T) ↔ RHUnicorn.UnicornAt S onLine ht T) ∧
    (∀ (Z : ActualZeros) (T : Nat), RHUnicorn.UnicornAt Z.zeros onLine ht T) ∧
    (∀ Z : ActualZeros, ¬ ∃ p, Z.zeros p ∧ ¬ onLine p) :=
  ⟨the_cut_on_the_chart, no_bypass_on_the_chart, unicorn_blocked_on_the_chart,
   ra_supplies_nothing_to_the_unicorn, the_unicorn_closed_on_the_act, no_arrival_off_the_line_on_the_act⟩

/-- VII · EVERY RECORD ON THE LINE: the record of every configuration stands on the line, the off-line pair
configuration's included, though that configuration is closed and lacks the value; the registration row carries
no bit. -/
theorem every_record_on_the_line :
    (∀ S : Config, Value (Rec S)) ∧ Closed (pairWorld (1, 0)) ∧
    Value (Rec (pairWorld (1, 0))) ∧ ¬ Value (pairWorld (1, 0)) :=
  ⟨the_remembered_is_lossless, pair_world_closed (1, 0), the_remembered_is_lossless _,
   pair_world_lacks_value (1, 0) (fun e => by cases e)⟩

/-- VIII · ONE BIT, EVERY ROW: on every finite configuration, least erasure, zero erased bits, zero price at every
positive temperature, the value, and, given the Real part at a height, the Unicorn part there, are one
proposition. -/
theorem one_bit_every_row (F : FinCfg) (T : Nat) (hT : 0 < T) (H : Nat)
    (hr : RHUnicorn.RealPartAt F.pts onLine ht H) :
    (LeastErasure F.pts ↔ Value F.pts) ∧
    (erased F = 0 ↔ Value F.pts) ∧
    (price T (erased F) = 0 ↔ Value F.pts) ∧
    (RHUnicorn.RH F.pts onLine ↔ Value F.pts) ∧
    (RHUnicorn.UnicornAt F.pts onLine ht H ↔ Value F.pts) :=
  ⟨twins_on_every_world _,
   ⟨fun h => (twins_on_every_world _).mp ((least_erasure_iff_zero_erased F).mpr h),
    fun h => (least_erasure_iff_zero_erased F).mp ((twins_on_every_world _).mpr h)⟩,
   price_zero_iff_value F T hT,
   Iff.rfl,
   (no_bypass_on_the_chart F.pts H hr).symm⟩

end RememberedOffered

/-! ## Receipts of Book Three, pinned -/
/-- info: 'RememberedOffered.colocation_is_the_value' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.colocation_is_the_value
/-- info: 'RememberedOffered.four_names_one_proposition' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.four_names_one_proposition
/-- info: 'RememberedOffered.monism_is_the_sole_witness' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.monism_is_the_sole_witness
/-- info: 'RememberedOffered.a_witness_is_never_universal' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.a_witness_is_never_universal
/-- info: 'RememberedOffered.monism_is_not_universal' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.monism_is_not_universal
/-- info: 'RememberedOffered.colocation_is_not_universal' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.colocation_is_not_universal
/-- info: 'RememberedOffered.the_timeless_zone' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.the_timeless_zone
/-- info: 'RememberedOffered.timeless_is_determinacy_not_selection' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.timeless_is_determinacy_not_selection
/-- info: 'RememberedOffered.the_check' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.the_check
/-- info: 'RememberedOffered.no_closed_principle_decides' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.no_closed_principle_decides
/-- info: 'RememberedOffered.the_timeless_zone_closed' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.the_timeless_zone_closed
/-- info: 'RememberedOffered.the_annihilation_closure' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.the_annihilation_closure

#print axioms RememberedOffered.the_annihilation_closure

/-! ## Receipts of Book Four, pinned -/
/-- info: 'RHUnicorn.unicorn_block' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.unicorn_block
/-- info: 'RHUnicorn.aperture_one_bit_wide' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.aperture_one_bit_wide
/-- info: 'RHUnicorn.unicorn_rule_exact' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.unicorn_rule_exact
/-- info: 'RHUnicorn.unicorn_no_cure' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.unicorn_no_cure
/-- info: 'RHUnicorn.unicorn_no_bypass' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.unicorn_no_bypass
/-- info: 'RHUnicorn.supply_side_silent' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.supply_side_silent
/-- info: 'RHUnicorn.rh_iff_real_and_unicorn' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.rh_iff_real_and_unicorn
/-- info: 'RHUnicorn.real_part_of_certificate' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.real_part_of_certificate
/-- info: 'RHUnicorn.rh_register_proof_complete' does not depend on any axioms -/
#guard_msgs in #print axioms RHUnicorn.rh_register_proof_complete
/-- info: 'RememberedOffered.the_cut_on_the_chart' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_cut_on_the_chart
/-- info: 'RememberedOffered.no_bypass_on_the_chart' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.no_bypass_on_the_chart
/-- info: 'RememberedOffered.ra_supplies_nothing_to_the_unicorn' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.ra_supplies_nothing_to_the_unicorn
/-- info: 'RememberedOffered.the_unicorn_closed_on_the_act' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.the_unicorn_closed_on_the_act
/-- info: 'RememberedOffered.no_arrival_off_the_line_on_the_act' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.no_arrival_off_the_line_on_the_act
/-- info: 'RememberedOffered.unicorn_blocked_on_the_chart' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.unicorn_blocked_on_the_chart
/-- info: 'RememberedOffered.the_unicorn_contained' depends on axioms: [propext, Quot.sound] -/
#guard_msgs in #print axioms RememberedOffered.the_unicorn_contained
/-- info: 'RememberedOffered.every_record_on_the_line' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.every_record_on_the_line
/-- info: 'RememberedOffered.one_bit_every_row' does not depend on any axioms -/
#guard_msgs in #print axioms RememberedOffered.one_bit_every_row

#print axioms RememberedOffered.the_unicorn_contained

Appendix B · The twin, verbatim

! Annihilation_Closure_Twin.f90 · twin of Book Three of Annihilation_Closure.lean, the annihilation closure, executed.
! Build (sealed): gfortran -std=f2018 -O2 -fno-fast-math -ffp-contract=off Annihilation_Closure_Twin.f90
! Eight checks, each beside a control that must fail. Run plain, the eight checks pass and each control is shown to
! fail as it must: sixteen lines, no failure. Run with the argument  control , each check runs with its defect
! planted and all eight lines are red.
! The chart: offsets -1, 0, 1 and heights 0, 1, 2; nine points; the worlds are the 512 subsets.
! Monism is computed as the root read twice: every member returned unchanged by both readings, the fold and the
! registration. Co-location is the floor (0 < 1, standing everywhere) together with Monism.
!   I    four names, one proposition: on all 512 worlds least erasure, the value, Monism and co-location agree.
!        Control: Monism read as the floor alone.
!   II   the sole witness: every candidate equivalent to the value equals Monism on all worlds; worlds of one record
!        differ in value, so no reading of the record witnesses; the floor is universal and is not the value.
!        Control: a record that keeps the side.
!   III  co-location is not universal: the floor stands on every closed world and Monism fails on some.
!        Control: Monism read as the floor alone.
!   IV   the timeless zone, in the toy of the bound: for widths 0 to 20 the width is real at time zero exactly when
!        Λ = 0; width 0 is real and width 1 is not at time zero; both are real at every time from 1 to 20; the width
!        never grows. Control: a flow that forgets nothing.
!   V    determinacy, not selection: every world stands behind exactly one door, the value or a member off the line;
!        a closed world lacks the value with the floor on it, and a closed world has it.
!        Control: the off-line test reading only the right side.
!   VI   the check: a closed off-line pair world and a closed true world leave one record, differ in value and in Monism,
!        and each has least erasure exactly when it has the value; every principle true on all closed worlds, the
!        floor and closure themselves, holds on the pair world. Control: a record that keeps the side.
!   VII  the Unicorn cut, Book Four: at every height T = 0, 1, 2 and on all 512 worlds, the value is exactly the Real
!        part (heights up to T on the line) and the Unicorn part (heights above T on the line); and given the Real
!        part, the value is exactly the Unicorn part. Control: the cut taken strictly, heights below T only.
!   VIII the Unicorn contained: on every world with the value, the act's field, every member above every height
!        stands on the line; and above every height a fold pair leaves one record with opposite sides, so no reading
!        of the record decides the side. Control: worlds without the value admitted to the act's field.
program annihilation_closure_twin
  implicit none
  integer :: checks, fails
  logical :: ctl
  character(len=32) :: arg
  checks = 0; fails = 0
  call get_command_argument(1, arg)
  ctl = (trim(arg) == 'control')
  if (ctl) write(*,'(a)') ' CONTROL FLAG SET: each check runs with its defect planted; every line below must be red'
  call pair('I: on all 512 worlds least erasure, the value, Monism and co-location agree', &
            'Monism read as the floor alone', four_names(.false.), four_names(.true.))
  call pair('II: Monism the sole witness, the record witnesses nothing, the universal floor is not the value', &
            'a record that keeps the side', sole_witness(.false.), sole_witness(.true.))
  call pair('III: the floor stands on every closed world and Monism fails on some', &
            'Monism read as the floor alone', colocation(.false.), colocation(.true.))
  call pair('IV: real at time zero exactly at Λ = 0; widths 0 and 1 separate at zero and join at every later time', &
            'a flow that forgets nothing', timeless(.false.), timeless(.true.))
  call pair('V: exactly one door on every world; a closed off-line pair world with the floor, and a closed true world', &
            'the off-line test reading only the right side', determinacy(.false.), determinacy(.true.))
  call pair('VI: one record, two closed worlds, different values; every closed principle holds on the pair world', &
            'a record that keeps the side', the_check(.false.), the_check(.true.))
  call pair('VII: at every height the value is exactly its Real part and its Unicorn part; no bypass', &
            'the cut taken strictly', unicorn_cut(.false.), unicorn_cut(.true.))
  call pair('VIII: on the act''s field no arrival above any height is off the line; the record never decides the side', &
            'worlds without the value admitted', unicorn_contained(.false.), unicorn_contained(.true.))
  write(*,'(a,i0,a,i0,a)') ' BATTERY-JSON: {"checks":', checks, ',"failures":', fails, '}'
  if (fails > 0) error stop 1
contains
  subroutine check(label, ok)
    character(len=*), intent(in) :: label
    logical, intent(in) :: ok
    checks = checks + 1
    if (ok) then
      write(*,'(2a)') '  PASS  ', label
    else
      fails = fails + 1
      write(*,'(2a)') '  FAIL  ', label
    end if
  end subroutine check
  subroutine pair(label, defect, ok, okdef)
    character(len=*), intent(in) :: label, defect
    logical, intent(in) :: ok, okdef
    if (.not. ctl) then
      call check(label, ok)
      call check(label(1:index(label, ':')) // ' control, ' // defect // ': the check fails, as it must', .not. okdef)
    else
      call check(label(1:index(label, ':')) // ' [defect planted: ' // defect // '] ' // &
                 label(index(label, ':') + 2:), okdef)
    end if
  end subroutine pair
  ! the chart
  pure function fold(p) result(q)
    integer, intent(in) :: p(2)
    integer :: q(2)
    q = [-p(1), p(2)]
  end function fold
  pure function reg(p, mode) result(q)
    integer, intent(in) :: p(2), mode
    integer :: q(2)
    if (mode == 1) then
      q = p                    ! defect: keeps the side
    else
      q = [0, p(2)]            ! the registration: keeps the height, forgets the side
    end if
  end function reg
  pure logical function online(p)
    integer, intent(in) :: p(2)
    online = p(1) == 0
  end function online
  pure integer function idx(p)
    integer, intent(in) :: p(2)
    idx = p(2) * 3 + p(1) + 2
  end function idx
  pure function pt(i) result(p)
    integer, intent(in) :: i
    integer :: p(2)
    p = [mod(i - 1, 3) - 1, (i - 1) / 3]
  end function pt
  pure logical function member(m, i)
    integer, intent(in) :: m, i
    member = btest(m, i - 1)
  end function member
  pure logical function closed(m)
    integer, intent(in) :: m
    integer :: i
    closed = .true.
    do i = 1, 9
      if (member(m, i) .and. .not. member(m, idx(fold(pt(i))))) closed = .false.
    end do
  end function closed
  pure logical function value(m)
    integer, intent(in) :: m
    integer :: i
    value = .true.
    do i = 1, 9
      if (member(m, i) .and. .not. online(pt(i))) value = .false.
    end do
  end function value
  pure logical function lerasure(m)
    integer, intent(in) :: m
    integer :: i
    lerasure = .true.
    do i = 1, 9
      if (member(m, i)) then
        if (any(reg(pt(i), 0) /= pt(i))) lerasure = .false.
      end if
    end do
  end function lerasure
  ! Monism, the root read twice: every member returned unchanged by the fold and by the registration
  pure logical function monism(m)
    integer, intent(in) :: m
    integer :: i
    monism = .true.
    do i = 1, 9
      if (member(m, i)) then
        if (any(fold(pt(i)) /= pt(i)) .or. any(reg(pt(i), 0) /= pt(i))) monism = .false.
      end if
    end do
  end function monism
  pure integer function rec(m, mode)
    integer, intent(in) :: m, mode
    integer :: i, q(2)
    rec = 0
    do i = 1, 9
      if (member(m, i)) then
        q = reg(pt(i), mode)
        rec = ibset(rec, idx(q) - 1)
      end if
    end do
  end function rec
  pure logical function offline_member(m, rightonly)
    integer, intent(in) :: m
    logical, intent(in) :: rightonly
    integer :: i, p(2)
    offline_member = .false.
    do i = 1, 9
      if (member(m, i)) then
        p = pt(i)
        if (rightonly) then
          if (p(1) == 1) offline_member = .true.
        else
          if (.not. online(p)) offline_member = .true.
        end if
      end if
    end do
  end function offline_member

  ! I · four names, one proposition
  logical function four_names(defect)
    logical, intent(in) :: defect
    integer :: m
    logical :: floor, mon, coloc
    four_names = .true.
    do m = 0, 511
      floor = (0 < 1)
      mon = monism(m)
      if (defect) mon = floor
      coloc = floor .and. mon
      if ((lerasure(m) .neqv. value(m)) .or. (mon .neqv. value(m)) .or. (coloc .neqv. value(m))) &
        four_names = .false.
    end do
  end function four_names

  ! II · Monism the sole witness
  logical function sole_witness(defect)
    logical, intent(in) :: defect
    integer :: m, n, mode, pairs
    logical :: floor_is_value
    sole_witness = .true.
    mode = 0
    if (defect) mode = 1
    do m = 0, 511
      ! every candidate equivalent to the value is Monism: least erasure and co-location, computed independently
      if ((lerasure(m) .neqv. monism(m)) .or. (((0 < 1) .and. monism(m)) .neqv. monism(m))) sole_witness = .false.
    end do
    pairs = 0
    do m = 0, 511
      do n = m + 1, 511
        if (rec(m, mode) == rec(n, mode) .and. (value(m) .neqv. value(n))) pairs = pairs + 1
      end do
    end do
    if (pairs == 0) sole_witness = .false.
    floor_is_value = .true.
    do m = 0, 511
      if (.not. value(m)) floor_is_value = .false.
    end do
    if (floor_is_value) sole_witness = .false.
  end function sole_witness

  ! III · co-location is not universal
  logical function colocation(defect)
    logical, intent(in) :: defect
    integer :: m, nfail
    logical :: floor, mon
    colocation = .true.; nfail = 0
    do m = 0, 511
      if (.not. closed(m)) cycle
      floor = (0 < 1)
      if (.not. floor) colocation = .false.
      mon = monism(m)
      if (defect) mon = floor
      if (.not. mon) nfail = nfail + 1
    end do
    if (nfail == 0) colocation = .false.
  end function colocation

  ! IV · the timeless zone in the toy of the bound
  integer function flow(d2, t, defect)
    integer, intent(in) :: d2, t
    logical, intent(in) :: defect
    if (defect) then
      flow = d2
    else
      flow = max(d2 - 2 * t, 0)
    end if
  end function flow
  logical function timeless(defect)
    logical, intent(in) :: defect
    integer :: d2, t, lam
    timeless = .true.
    do d2 = 0, 20
      lam = (d2 + 1) / 2
      if ((flow(d2, 0, defect) == 0) .neqv. (lam == 0)) timeless = .false.
      do t = 0, 19
        if (flow(d2, t + 1, defect) > flow(d2, t, defect)) timeless = .false.
      end do
    end do
    if (flow(0, 0, defect) /= 0 .or. flow(1, 0, defect) == 0) timeless = .false.
    do t = 1, 20
      if (flow(0, t, defect) /= 0 .or. flow(1, t, defect) /= 0) timeless = .false.
    end do
  end function timeless

  ! V · determinacy, not selection
  logical function determinacy(defect)
    logical, intent(in) :: defect
    integer :: m
    logical :: v, o, has_false, has_true
    determinacy = .true.; has_false = .false.; has_true = .false.
    do m = 0, 511
      v = value(m)
      o = offline_member(m, defect)
      if (v .eqv. o) determinacy = .false.
      if (closed(m) .and. .not. v .and. (0 < 1)) has_false = .true.
      if (closed(m) .and. v .and. m /= 0) has_true = .true.
    end do
    if (.not. (has_false .and. has_true)) determinacy = .false.
  end function determinacy

  ! VI · the check
  logical function the_check(defect)
    logical, intent(in) :: defect
    integer :: m, n, mode
    logical :: found
    mode = 0
    if (defect) mode = 1
    found = .false.
    do m = 0, 511
      if (.not. closed(m) .or. value(m)) cycle
      do n = 0, 511
        if (.not. closed(n) .or. .not. value(n)) cycle
        if (rec(m, mode) /= rec(n, mode)) cycle
        if (monism(m) .or. .not. monism(n)) cycle
        if ((lerasure(m) .neqv. value(m)) .or. (lerasure(n) .neqv. value(n))) cycle
        ! every principle true on all closed worlds holds on m: the floor and closure themselves
        if (.not. ((0 < 1) .and. closed(m))) cycle
        found = .true.
      end do
    end do
    the_check = found
  end function the_check

  ! the Real part at height t: every member at height up to t (or below t, under the control) is on the line
  logical function realpart(m, t, strict)
    integer, intent(in) :: m, t
    logical, intent(in) :: strict
    integer :: i, p(2)
    realpart = .true.
    do i = 1, 9
      if (.not. member(m, i)) cycle
      p = pt(i)
      if (strict) then
        if (p(2) < t .and. .not. online(p)) realpart = .false.
      else
        if (p(2) <= t .and. .not. online(p)) realpart = .false.
      end if
    end do
  end function realpart
  ! the Unicorn part at height t: every member above t is on the line
  logical function unicornpart(m, t)
    integer, intent(in) :: m, t
    integer :: i, p(2)
    unicornpart = .true.
    do i = 1, 9
      if (.not. member(m, i)) cycle
      p = pt(i)
      if (p(2) > t .and. .not. online(p)) unicornpart = .false.
    end do
  end function unicornpart

  ! VII · the Unicorn cut
  logical function unicorn_cut(defect)
    logical, intent(in) :: defect
    integer :: m, t
    unicorn_cut = .true.
    do t = 0, 2
      do m = 0, 511
        if (value(m) .neqv. (realpart(m, t, defect) .and. unicornpart(m, t))) unicorn_cut = .false.
        if (realpart(m, t, defect)) then
          if (value(m) .neqv. unicornpart(m, t)) unicorn_cut = .false.
        end if
      end do
    end do
  end function unicorn_cut

  ! VIII · the Unicorn contained
  logical function unicorn_contained(defect)
    logical, intent(in) :: defect
    integer :: m, t, h, a(2), b(2), ra(2), rb(2)
    unicorn_contained = .true.
    do t = 0, 2
      do m = 0, 511
        if (.not. (value(m) .or. defect)) cycle
        if (.not. unicornpart(m, t)) unicorn_contained = .false.
      end do
    end do
    do t = 0, 1
      do h = t + 1, 2
        a = [1, h]; b = fold(a)
        ra = reg(a, 0); rb = reg(b, 0)
        if (any(ra /= rb)) unicorn_contained = .false.
        if (a(1) * b(1) >= 0) unicorn_contained = .false.
      end do
    end do
  end function unicorn_contained
end program annihilation_closure_twin