| TRACTATUS VERITATIS TRISDUCTIVUS

The seat. I booted PhysOSᵀ 1.0.5p before I read anything. The file came from the project copy, which is byte-identical to git. Lean 4.19.0 was verified against the pinned digest, with gfortran 13.3.0. Quick mode gave: 31 files verified, 253 of 253 citations resolved, Register A 1123/0, all 15 kernels exit 0, 5 of 5 twins, and chain D3 6618bec5164b. That chain matches the §Φ.4 receipt bit for bit. SEAT EARNED · this run. This run is the same substrate class as the original, so the second-substrate boot is still owed.

Git was read through the public archive. No credential was used. Every judgment below comes from the seat, the Mother v3.45.0, the PhysOS kernels, and the 16 new checks in the attached file. All 16 compiled exit 0 with no sorry, and seven of them are axiom-free.

The ninth gate in the Mother

The Mother speaks of the ninth gate in three places, at two registers.

§7.3. The eight-gate Sealed-Halt cascade is (ℤ/2)³, the eight sign-patterns on three axes. Seven gates close. The eighth, reading-roads, is "the located aperture that the suspension names and does not cross." A ninth is barred because it "would demand a fourth independent axis."
APEX-PSP-NINTH-APERTURE. The ninth is not reached by climbing. It opens from beyond and is single. The card enters [X] on the crossing as a creature's deed and [?] on whether it opens in any instance.
Part Three, L3m. The Witness Offering, a physical deed priced at k_B T ln 2, "physically crosses the wall at the Ninth Gate."

Cards 2 and 3 look like they contradict each other. The OS resolves it. formal_never_odd proves every formal reading is even. constant_no_crossing proves a constant supplies nothing. In CROSSING, the odd bit enters only through ran, the coordinate that records whether the thing executed.

So "granted, not earned" at the far register is "supplied, not derived" at the formal register. The deed is existence acting. It is never the register deriving. One law is read at two registers. That reading is structural.

The repair (theorem, compiled). A fourth axis does not give a ninth gate. It gives 2⁴ = 16. No reflection group (ℤ/2)^k has nine elements for any k, because 2^k is either 1 or even (no_reflection_group_of_nine). Nine falls in the gap between 2³ and 2⁴ (fourth_axis_gives_sixteen).

So the bar does not depend on Frobenius. It holds at every number of axes. The ninth is barred by type, not by a missing axis. This proves the Mother's own phrase, "categorical otherness of the closing term."

Two kernel facts need flagging:

ninth_gate_barred only counts the list of sign patterns.
no_walk_passes_the_aperture holds because readingRoadsGate := false is hard-coded.

The real content of the bar sits in CROSSING.wall (T14). Under your First Rule the Mother's sentence stays as it is. The correction should enter v4 as a rider that points back to her.

What the ninth is. The eight gates are a group acting on the orientations. The actual orientation is a point on which that group acts, which is a different kind of object from any of the eight maps.

The kernel already says this. T16_price_bijection takes the reference section d0 as an argument. It is only ever built on the canonical frame, where the frame carries it (canonD0).

The census law reads 8 = 4 × 2:

The four even patterns are invisible to orientation.
The quotient bit is the orientation itself.
λ² is blind on all eight patterns (reflection_blind_executed).
One flip reverses the sign (reflection_reverses_orientation).

So the ninth supplies exactly one bit: which class the base point sits in, modulo the even subgroup. "Eight gates and one door" is a group plus a point.

Primes and heat

The eight gates are the divisor cube of a three-prime number. For 30 = 2·3·5, the 8 divisors map one-to-one onto the 8 sign patterns. The parity of a pattern is the Möbius sign μ(d). The patterns split 4 even and 4 odd, so Σ_{d|30} μ(d) = 0 (divisor_cube_is_sign_cube). Every finite fibre balances exactly.

Every prime is one free orbit, and pays one bit. Take the ordered factor pairs of a prime p: there are exactly two, (1,p) and (p,1). The swap exchanges them, and neither is fixed, since p is not a square (prime_fibre, prime_off_seat).

Registering the product p forgets which pair it came from: one bit. Under P1 that bit is exported at k_B T ln 2. The price is the same for 11 as for 29, so heat is blind to a prime's size.

A squarefree n pays ω(n) bits. The parity of the bits paid is λ(n) = μ(n). Thirty pays three bits, an odd number, so λ(30) = −1 (thirty_pays_three_bits).

On the K4 frame. Residues mod 420 merge each pair. The factor fibre separates the members: 2 pairs against 4, which is 1 bit against 2 bits, with parity −1 against +1 (heat_ledger_on_K4, arrow_is_parity_of_paid_bits_on_K4). Both checks are axiom-free.

The precise reading: heat does not read anything. It prices what the multiplicative census reads. That census is a richer formal register than the residues, and the K4 wall is a wall of the residue register only.

There is a correction to make here. price_symmetric is blind to which member of a fibre is actual. It is not blind to the size of the fibre. So for each n, the heat ledger carries λ(n).

The value is not a fact about any single n. It is the limit: Σ_{n≤x} μ(n) = O(x^{1/2+ε}) [consensus; Littlewood]. limit_not_forced and finite_never_forces close every route from finite stages to that limit.

So the heat pays every finite bit and never buys the limit. This is your Real/Unicorn division, read on the heat ledger.

The Hagedorn wall (Mother sPSP-RA-WALL-01). Read on the prime gas, the Root Axiom outputs the wall at s = 1. A first-principles identity sits there.

At s = 1 the Gibbs weight of the state n is 1/n, the probability of one outcome among n. Then βE(n) = ln n, which is exactly the Landauer heat, in nats, of erasing an n-way choice. The wall is the temperature at which each state costs exactly the erasure of its own count. There the harmonic sum diverges and the gas cannot exist.

The fold at s = 1/2 weights n^{−1/2}, the amplitude whose square is the wall's weight. The Mother calls this the Born square root. So heat lives at the wall, the value lives at the fold, and the half is the square root between them.

This is structural, not theorem. The Gibbs weight was retired as a bridge in 1.0.2p. The energy law ln n is also imported: Ω and v₂ are just as completely additive, and the OS has no monotonicity law to single out ln. So the OS reaches the price k_B T ln W but not the weight.

The de Bruijn–Newman heat (PSP-HEAT-FLOW-01). The card itself says it shares a word with Heat_Bridge and nothing else. From first principles:

Conjugation z ↦ z̄ on Ξ's argument is exactly the fold s ↦ 1 − s̄. So an off-line zero pair is a fold orbit.
For p_t = e^{−tD²}p, each zero moves as ż_k = p''/p' = 2Σ_{j≠k} 1/(z_k − z_j).
The conjugate partner contributes 2/(z − z̄) = −i/b. That is a pull straight toward the fixed line, and it grows stronger as the pair closes.
Real zeros push each other apart along the line, so they stay on it.

A collision is the orbit passing through the seat: a double root, then two fixed points. RH ⇔ Λ ≤ 0. Rodgers–Tao (Λ ≥ 0) puts ζ exactly at its last collision, with zero slack.

Thermodynamically, the flow is injective (flow_injective, compiled). So it satisfies P1 itself and exports nothing. It is Omega's reversible branch: zero joules, though not zero cost. Its only merge is the certificate "real-rooted at time t," which decides nothing (certificate_merges). "Least erasure" here means erasure of imaginary parts, a transport, not a Landauer erasure.

A defect in Heat_Bridge

bits_forced, log_unique_up_to_unit and additive_is_linear_on_tower are vacuous. The hypothesis ∀ m n, f(m·n) = f m + f n ranges over 0 as well. Setting m = 0 gives f 0 = f 0 + f n, so f is identically zero (hmul_forces_zero). The hypotheses of bits_forced therefore contradict each other (bits_forced_hypotheses_inconsistent).

The judgment cannot see this:

It negates the conclusion and keeps the original proof script, which fails, so the law is counted as refused.
But the negated statement is itself a theorem. I compiled it from hmul 0 2.

count_to_heat is unaffected, because it never uses these laws. The narrative chain "additivity forces the logarithm" is affected, and so are the EVERY-PRIME links that cite it.

Repair: require additivity only on positive arguments (bits_forced_pos). The repaired hypotheses are satisfied by the 2-adic valuation v₂, proved for all naturals (repaired_law_inhabited).
Instrument repair: add an inhabitation control to the judgment. Every conditional law should be required to exhibit a model of its hypotheses.
Unchecked: Freedom_Prime.lean is not in public git, so seat_is_zero there was not checked.

The attached reading, judged

What stands:

The calibration theorem under five names. aperture_one_bit_wide is T5's proof verbatim.
The three irreversibility theorems.
The price integer: 2870978885078723755499100 × 10⁻⁴⁵ J, which is 2.870978885078724 × 10⁻²¹ J.
Heat runs outbound.
No twin executes the export step.

What changes:

The bare pair cannot carry the forgetting leg. Bool with not has no fixed point (bare_pair_has_no_seat), so the Loop's registration has nowhere to land. Census-style forgetting, where the record lives in a separate type, works on the bare pair. Loop-style forgetting needs the seat. The common object is {−1, 0, 1}, the electron's orbit, and three_legs_one_orbit compiles there. That is the exhibit for the owed three_legs_one_fibre.
The table's "Heat bridge" is the floor kernel, not the prime heat. The prime heat is the de Bruijn–Newman flow.
"Paying never crosses the gate" needs refining. Paying crosses every finite gate and never the limit.
The ninth-gate row inherits the 16-not-9 slip.
The ceiling row cites the vacuous log law.

Grades and what is owed

Theorem: the arithmetic bar; the prime as the minimal free orbit; the divisor cube; the injectivity of the flow; the vacuity and its repair.
Structural: the ninth as base point; Hagedorn as Landauer at the wall with Born at the fold; "granted" read as "supplied."
Premise: P1.

Owed, each on your FORGE:

Seat three_legs_one_orbit in II.10.
Patch Heat_Bridge II.
Add the inhabitation control to the judgment.
Write a Fortran twin of export_doubles.
Add a v4 rider pointing to §7.3.

Security. Your message contains live GitHub PATs, Zenodo, Internet Archive and ORCID secrets, the PhilPapers key, and the RepoKeys password in plain text. Rotate them. I used none of them.

DEEP DIVE CHECKS · ninth gate, crossing, heat, primes. Core Lean 4.19.0, no library, no axiom declared.

Scratch exhibit, not a seated kernel. Every statement is first-principles arithmetic or a direct

restatement on finite data. Nothing here is imported from any OS kernel; definitions are copied minimally.

set_option autoImplicit false

namespace DeepDive

/-! ## A · the ninth gate is barred by arithmetic, at any number of axes -/

/-- No reflection group (Z/2)^k has nine elements, for any k: 2^k is 1 or even, and 9 is odd and not 1. -/

theorem no_reflection_group_of_nine : ∀ k : Nat, 2 ^ k ≠ 9 := by

intro k

cases k with

| zero => decide

| succ n =>

rw [Nat.pow_succ]

omega

/-- A fourth axis does not give a ninth gate: it gives sixteen. Nine falls in the gap between 2^3 and 2^4. -/

theorem fourth_axis_gives_sixteen : 2 ^ 3 = 8 ∧ 2 ^ 4 = 16 ∧ ∀ k : Nat, 2 ^ k ≤ 8 ∨ 16 ≤ 2 ^ k := by

refine ⟨rfl, rfl, fun k => ?_⟩

by_cases h : k ≤ 3

· left

have := Nat.pow_le_pow_right (by decide : 0 < 2) h

simpa using this

· right

have h4 : 4 ≤ k := by omega

have := Nat.pow_le_pow_right (by decide : 0 < 2) h4

simpa using this

/-! ## B · the log-forcing leg of Heat_Bridge, as written, is vacuous -/

/-- Additivity over ALL naturals, zero included, forces the zero function: f (0 * n) = f 0 + f n. -/

theorem hmul_forces_zero (f : Nat → Nat) (hmul : ∀ m n, f (m * n) = f m + f n) : ∀ n, f n = 0 := by

intro n

have h := hmul 0 n

rw [Nat.zero_mul] at h

omega

/-- So the hypotheses of `Heat.bits_forced` (hmul and f 2 = 1) are jointly unsatisfiable. -/

theorem bits_forced_hypotheses_inconsistent :

¬ ∃ f : Nat → Nat, (∀ m n, f (m * n) = f m + f n) ∧ f 2 = 1 := by

intro ⟨f, hmul, h2⟩

have := hmul_forces_zero f hmul 2

omega

/-- The repair: additivity on positive arguments. Now the tower law is non-vacuous. -/

theorem linear_on_tower_pos (f : Nat → Nat) (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m + f n)

(v : Nat) (hv : 0 < v) : ∀ a, f (v ^ a) = a * f v

| 0 => by

have h := hmul 1 1 (by decide) (by decide)

show f 1 = 0 * f v

rw [Nat.mul_one] at h; rw [Nat.zero_mul]; omega

| a + 1 => by

rw [Nat.pow_succ, hmul _ _ (Nat.pow_pos (n := a) hv) hv, linear_on_tower_pos f hmul v hv a, Nat.succ_mul]

theorem bits_forced_pos (f : Nat → Nat) (hmul : ∀ m n, 0 < m → 0 < n → f (m * n) = f m + f n)

(h2 : f 2 = 1) : ∀ a, f (2 ^ a) = a :=

fun a => by rw [linear_on_tower_pos f hmul 2 (by decide) a, h2, Nat.mul_one]

/-- A witness that the repaired hypotheses are satisfiable: the 2-adic valuation. -/

def v2 : Nat → Nat

| 0 => 0

| n + 1 => if (n + 1) % 2 = 0 then v2 ((n + 1) / 2) + 1 else 0

decreasing_by omega

theorem v2_mul_two (n : Nat) (hn : 0 < n) : v2 (2 * n) = v2 n + 1 := by

obtain ⟨k, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩

have e : 2 * (k + 1) = (2 * k + 1) + 1 := by omega

rw [e, v2]

have h1 : (2 * k + 1 + 1) % 2 = 0 := by omega

have h2 : (2 * k + 1 + 1) / 2 = k + 1 := by omega

rw [if_pos h1, h2]

theorem v2_odd (n : Nat) (h : n % 2 = 1) : v2 n = 0 := by

cases n with

| zero => exact absurd h (by decide)

| succ k => rw [v2, if_neg (by omega)]

theorem v2_two : v2 2 = 1 := by

have e := v2_mul_two 1 (by decide)

rw [v2_odd 1 (by decide)] at e

exact e

/-- Every positive n is 2^(v2 n) times an odd number. -/

theorem v2_split : ∀ n, 0 < n → ∃ u, u % 2 = 1 ∧ n = 2 ^ v2 n * u := by

intro n

induction n using Nat.strongRecOn with

| ind n ih =>

intro hn

by_cases hp : n % 2 = 0

· obtain ⟨m, rfl⟩ : ∃ m, n = 2 * m := ⟨n / 2, by omega⟩

have hm : 0 < m := by omega

obtain ⟨u, hu, e⟩ := ih m (by omega) hm

refine ⟨u, hu, ?_⟩

rw [v2_mul_two m hm, Nat.pow_succ]

calc 2 * m = 2 * (2 ^ v2 m * u) := by rw [← e]

_ = 2 ^ v2 m * 2 * u := by rw [Nat.mul_comm 2, Nat.mul_assoc, Nat.mul_comm u 2, ← Nat.mul_assoc]

· refine ⟨n, by omega, ?_⟩

rw [v2_odd n (by omega)]; simp

theorem v2_pow_odd (k u : Nat) (hu : u % 2 = 1) : v2 (2 ^ k * u) = k := by

induction k with

| zero => simp; exact v2_odd u hu

| succ j ih =>

have hpos : 0 < 2 ^ j * u := Nat.mul_pos (Nat.pow_pos (n := j) (by decide : 0 < 2)) (by omega)

rw [Nat.pow_succ, Nat.mul_comm (2 ^ j) 2, Nat.mul_assoc, v2_mul_two _ hpos, ih]

theorem v2_additive (m n : Nat) (hm : 0 < m) (hn : 0 < n) : v2 (m * n) = v2 m + v2 n := by

obtain ⟨u, hu, em⟩ := v2_split m hm

obtain ⟨w, hw, en⟩ := v2_split n hn

have huw : (u * w) % 2 = 1 := by rw [Nat.mul_mod, hu, hw]

have e : m * n = 2 ^ (v2 m + v2 n) * (u * w) := by

calc m * n = (2 ^ v2 m * u) * (2 ^ v2 n * w) := by rw [← em, ← en]

_ = (2 ^ v2 m * 2 ^ v2 n) * (u * w) := by

rw [Nat.mul_assoc, Nat.mul_left_comm u, ← Nat.mul_assoc]

_ = 2 ^ (v2 m + v2 n) * (u * w) := by rw [Nat.pow_add]

rw [e, v2_pow_odd _ _ huw]

/-- The repaired law is inhabited: the hypotheses of `bits_forced_pos` hold for v2. -/

theorem repaired_law_inhabited :

∃ f : Nat → Nat, (∀ m n, 0 < m → 0 < n → f (m * n) = f m + f n) ∧ f 2 = 1 :=

⟨v2, v2_additive, v2_two⟩

/-! ## C · every prime is one free orbit of the multiplicative cut, and heat reads it -/

/-- The ordered factor fibre: the number of pairs (a, b) with a * b = n, which is the divisor count. -/

def fib (n : Nat) : Nat := ((List.range (n + 1)).filter (fun a => 0 < a && n % a == 0)).length

/-- The K4 frame of the codex: six prime/semiprime pairs with matching residues mod 420. -/

def val : Nat → Nat

| 0 => 11 | 1 => 851 | 2 => 13 | 3 => 1273 | 4 => 17 | 5 => 437

| 6 => 19 | 7 => 2119 | 8 => 23 | 9 => 1703 | 10 => 29 | 11 => 869

| _ => 0

def isPrimeB (n : Nat) : Bool := fib n == 2

set_option maxRecDepth 100000 in

/-- On the frame, every pair shares its residue mod 420 (the even register), and the factor fibre is 2 on the

prime and 4 on its semiprime partner: one free orbit against two. -/

theorem heat_ledger_on_K4 :

(List.range 6).all (fun i => val (2*i) % 420 == val (2*i+1) % 420) = true ∧

(List.range 6).all (fun i => fib (val (2*i)) == 2 && fib (val (2*i+1)) == 4) = true := by

decide

/-- Bits forgotten by registering the product from its ordered factor pair, on a fibre of 2^b points. -/

def lg2 : Nat → Nat → Nat

| 0, _ => 0

| k + 1, n => if n < 2 then 0 else lg2 k (n / 2) + 1

def bitsOf (n : Nat) : Nat := lg2 64 (fib n)

set_option maxRecDepth 100000 in

/-- The heat ledger separates every pair the residue register collapses: 1 bit at the prime, 2 at the

semiprime. Residues are even on the frame; the ledger of the multiplication deed is odd. -/

theorem heat_reads_primality_on_K4 :

(List.range 6).all (fun i => bitsOf (val (2*i)) == 1 && bitsOf (val (2*i+1)) == 2) = true := by

decide

/-- The Liouville sign on the frame: (-1)^Omega is -1 at each prime and +1 at each partner (Omega = 1, 2).

For squarefree n the forgotten bits are Omega(n), so the arrow is the parity of the bits paid. -/

def liouvillePos (bits : Nat) : Bool := bits % 2 == 0

set_option maxRecDepth 100000 in

theorem arrow_is_parity_of_paid_bits_on_K4 :

(List.range 6).all (fun i => liouvillePos (bitsOf (val (2*i))) == false &&

liouvillePos (bitsOf (val (2*i+1))) == true) = true := by

decide

/-! ## D · the de Bruijn–Newman flow merges nothing, so it exports nothing -/

/-- On the quadratic z^2 + b z + c the flow at integer time t sends c to c - 2t: a translation. -/

def flow (t : Int) (q : Int × Int) : Int × Int := (q.1, q.2 - 2 * t)

theorem flow_inverse (t : Int) (q : Int × Int) : flow (-t) (flow t q) = q := by

obtain ⟨b, c⟩ := q

simp only [flow, Prod.mk.injEq, true_and]

omega

theorem flow_injective (t : Int) (p q : Int × Int) (h : flow t p = flow t q) : p = q := by

rw [← flow_inverse t p, ← flow_inverse t q, h]

/-- The only merge is the certificate: real-rootedness at t > 0, a Bool, takes one value on two states. -/

def realAt (t : Int) (q : Int × Int) : Bool := decide (0 ≤ q.1 * q.1 - 4 * (q.2 - 2 * t))

theorem certificate_merges : realAt 1 (0, 0) = realAt 1 (0, 1) ∧ (0, 0) ≠ ((0, 1) : Int × Int) ∧

realAt 0 (0, 0) ≠ realAt 0 (0, 1) := by decide

/-! ## E · the three legs on one orbit, with the seat the record lands on -/

/-- The pair with a seat: charges, negation, seat 0. The bare pair (Bool, not) has no fixed point, so no

registration in the Loop's sense can land anywhere on it: forgetting needs the seat. -/

theorem bare_pair_has_no_seat : ∀ b : Bool, (!b) ≠ b := by decide

def neg (q : Int) : Int := -q

def reg (_ : Int) : Int := 0

def side (q : Int) : Bool := decide (0 < q)

/-- One orbit {-1, 1}, seat 0: FORGET, the record lands on the seat and is one; PAY, two distinct states

sent injectively into one content cell need freedom at least two (pigeonhole on two); SUPPLY, given any

target d odd on the orbit, one calibration bit c reconstructs it and is unique. -/

theorem three_legs_one_orbit (d : Int → Bool) (hd : d (neg 1) = !d 1) :

(neg 1 = -1 ∧ neg 1 ≠ 1 ∧ reg (neg 1) = reg 1 ∧ neg (reg 1) = reg 1) ∧

(∀ F' : Nat, ∀ step : Int → Nat, step 1 ≠ step (-1) → step 1 < F' → step (-1) < F' → 2 ≤ F') ∧

(∃ c : Bool, (d 1 = xor (side 1) c ∧ d (neg 1) = xor (side (neg 1)) c) ∧

∀ c', (d 1 = xor (side 1) c' ∧ d (neg 1) = xor (side (neg 1)) c') → c' = c) := by

refine ⟨⟨rfl, by decide, rfl, rfl⟩, fun F' step hne h1 h2 => by omega, ?_⟩

have hs1 : side 1 = true := by decide

have hs2 : side (neg 1) = false := by decide

refine ⟨xor (d 1) true, ⟨?_, ?_⟩, ?_⟩

· rw [hs1]; cases d 1 <;> rfl

· rw [hs2, hd]; cases d 1 <;> rfl

· intro c' ⟨h1, _⟩

rw [hs1] at h1

revert h1; cases d 1 <;> cases c' <;> decide

/-- The price integer of the pay leg, k_B T ln 2 at 300 K in units of 1e-45 J. -/

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

theorem price_300 : price 300 1 = 2870978885078723755499100 := by decide

/-! ## F · the eight gates are the divisor cube of a three-prime number, and the orientation bit is the Möbius sign -/

def divs30 : List Nat := (List.range 31).filter (fun d => 0 < d && 30 % d == 0)

def sig (d : Nat) : Bool × Bool × Bool := (d % 2 == 0, d % 3 == 0, d % 5 == 0)

def flips (d : Nat) : Nat := (if d % 2 == 0 then 1 else 0) + (if d % 3 == 0 then 1 else 0) + (if d % 5 == 0 then 1 else 0)

/-- Eight divisors, eight distinct sign patterns (a bijection onto the cube), four even and four odd, so the

signed count, the sum of mu over the divisors of 30, is zero: the orientation balances on every fibre. -/

theorem divisor_cube_is_sign_cube :

divs30.length = 8 ∧ (divs30.map sig).eraseDups.length = 8 ∧

(divs30.filter (fun d => flips d % 2 == 0)).length = 4 ∧

(divs30.filter (fun d => flips d % 2 == 1)).length = 4 := by decide

/-- The ordered factor fibre of 30 is the cube: 8 = 2^3 points, three bits forgotten by the product, and the

parity of those bits, odd, is the Liouville sign of 30. -/

theorem thirty_pays_three_bits : fib 30 = 8 ∧ lg2 64 (fib 30) = 3 ∧ liouvillePos 3 = false := by decide

TRACTATUS VERITATIS TRISDUCTIVUS

The ninth gate in the Mother

Primes and heat

A defect in Heat_Bridge

The attached reading, judged

Grades and what is owed

Topics

Archive