Foundation Public Spine

The public spine

The foundation public spine is the framework's honest map of its own results. It is a machine-checked collection of formal theorems that sorts every claim into one of two kinds: what the framework forces, and what it chooses. The sorting matters because the framework's central promise is that a small set of conditions on a cost function forces a unique answer, and the spine keeps that promise visible while marking where the framework must make a purchase.

The spine's first result is a tower of number systems. It proves that the natural numbers, the integers, and the rationals are all physically real, meaning they can be realized as structures in the framework. The real numbers are different. The spine proves that the continuum is not forced by the framework's delta-only rules; it must be added as a classical extension, a deliberate purchase. This is the first honest boundary: the framework does not pretend to derive the real line from nothing.

The spine also contains the cost selection theorem. It proves that any cost function satisfying five plain conditions, reciprocal symmetry, zero cost at unity, a composition law, calibration, and continuity, must equal J(x) = (x + 1/x)/2 - 1. This is the framework's keystone result, and the spine states it with a strength tag that marks it as a trace closure, meaning it relies on the completed real line. The spine's native version, proved on a countable carrier without continuity, is deposited separately, and the bridge between the two is itself shown to be a purchase.

The golden ratio emerges from the same reciprocal structure. The spine proves that phi is the unique self-similar scaling, and it shows that three of the four facts needed to derive phi come down to the delta-only rules. The fourth fact is where the completion is actually bought, and the spine proves it must be: no ratio orbit solves 1 + 1/x = x. The number phi is not a free choice; it is forced by the structure, but the step that completes the real line is a priced one.

The spine's most striking result is about linking in three dimensions. It proves that a circle embedded in a sphere detects nontrivial linking exactly when the sphere has three dimensions. The proof uses the AlexanderLinkingBridge, a fully inhabited theorem with zero axioms beyond the standard three, and it shows that the eight-tick cycle follows from this three-dimensional linking together with a period-eight pigeonhole argument. The spine is explicit that this is a topological theorem; the physical bridge from recognition to linking remains an open target.

What the spine changes is the way claims are read. It refuses untagged theorem badges, so every result carries its strength. The tower is forced; the continuum is purchased; the cost function is unique under its conditions; phi is forced but its completion is bought; three dimensions are forced by linking; the physical bridge is open. A reader can now see at a glance what the framework asserts as theorem and what it admits as choice.

theorem forced_tower_holds : Tagged StrengthTag.deltaOnly ForcedTower where
  holds := forcedTower

/-- Continuum cut: ℝ is not δ-forced. Classical uncountability lives here, so the
tag is `classicalExtension`, not `deltaOnly` (panel K2). -/
theorem continuum_is_purchase :
    Tagged StrengthTag.classicalExtension (¬ DeltaForced ℝ) where
  holds := not_deltaForced_real

theorem cost_selection_holds : Tagged StrengthTag.traceClosure CostSelectionPackage where
  holds := {
    j_unique := fun F _ hRecip hNorm hComp hCalib hCont {_x} hx =>
      law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont _ hx
  }

theorem phi_from_iota_holds :
    Tagged StrengthTag.traceClosure PhiFromIota where
  holds := { cost_and_scale := reciprocalGeneratorCert_holds }

/-- **The detection half is proved** (R2 of campaign P-d3link, 2026-07-17):
the flat unknot `z ↦ (z,0,0)` embeds S¹ in S³, and its complement retracts
onto the core circle `(0,0,w)`, so `H₁(S¹;ℤ) ≅ ℤ` (proved,
`circleH1ZIsoInt_holds`) is a retract of the complement's first homology,
which therefore is not zero. Real Mathlib singular homology throughout; no
arithmetic encoding anywhere in the proof
(`Foundation/UnknotComplementRetract.lean`). -/
theorem detectsNontrivialLinking_three : DetectsNontrivialLinking 3 :=
  ⟨UnknotComplementRetract.unknot, UnknotComplementRetract.unknot_isEmbedding,
    UnknotComplementRetract.unknotComplementH1_ne_zero
      CircleWindingChain.circleH1ZIsoInt_holds⟩

/-- The eight-tick target reduces to the D=3 bridge alone: the period half is
proved. -/
theorem target_eight_tick_of_bridge
    (h : target_D3_from_nonencoding_linking) : target_eight_tick_from_D3 :=
  ⟨h, cubePeriodEight_holds⟩

What this page does not claim

The physical recognition-to-linking bridge is not proved; it remains an open target. The real numbers are not forced by the framework's delta-only rules; they are a priced extension. The spine does not prove the Riemann Hypothesis or the fine-structure constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PublicSpine.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: