A registered result in its source context
Original ledger classification: Formal [F] (Lean kernel; no extra axioms)
Recorded statement: LEAN FORMALISATION of the anchor ladder and the Pascal ladder (hardening round, 2026-06-11): new modules TfptCarrier/AnchorLadder.lean and TfptCarrier/PascalLadder.lean, built and audited with the existing project (lake build 3353 jobs;…
Statement, assumptions and sources
Paper context: Verification safeguards
The exact identifier, original classification and full claim are available below.
The source wording and classification below are preserved as recorded. A paper link, shared script or authored topic relation does not upgrade the claim or report a new proof run. Read later reviewed findings separately.
Read the exact registered claim and its dependencies
FORM.LADDER.01
Original ledger classification: Formal [F] (Lean kernel; no extra axioms)
Original claim text
LEAN FORMALISATION of the anchor ladder and the Pascal ladder (hardening round, 2026-06-11): new modules TfptCarrier/AnchorLadder.lean and TfptCarrier/PascalLadder.lean, built and audited with the existing project (lake build 3353 jobs; scripts/audit.sh AUDIT: PASS - no sorry/axiom/unsafe, only the three standard kernel axioms). AnchorLadder: p_n(a) = 2 + 2^n for ALL n (general theorem, not a finite check); ladder atoms (3,4,6,10); p1p2p3 = 240; p4-p3 = 8; 240+8 = 248; binary ladder p_{n+1}-p_n = 2^n (general); elementary symmetric (4,5,2). PascalLadder: the odd-midpoint identity sum_{k<=K} C(2K+1,k) = 2^{2K} for ALL K (via Mathlib Nat.sum_range_choose_halfway - the ladder SOLVES side of v108 is now formal); bounded uniqueness for the carrier case K=2 on 1<=g<=40 (kernel-decidable); carrier world (5,16,3,8); neighbour worlds (K=1 one-family, K=3 nine-family, K=4 inconsistent 9 ndvd 255). Strengthens the [F] layer of v23/v106 (ladder) and v108 (Pascal ladder); the unbounded K=2 uniqueness remains covered by CarrierRankUniqueness (division-free form)
Original classification detail
Formal: anchor ladder general; Pascal ladder solves-side general + K=2 bounded uniqueness
Dependencies as recorded
ARCH.CORE.01; CAR.LADDER.01; FORM.P2.02
Open the original ledger source, row 192Location recorded in the ledger
These document locations are recorded directly on the ledger row. They are document level navigation, rather than a newly inferred section citation.
- Architecture, E8 and the electromagnetic fixed point
- E8 audit and bootstrap
Sections that explicitly cite this claim
A literal claim identifier is present in these paper sections. The section and its premises determine what the citation supports.
- Layer 6 — two independent reproduction pathsVerification safeguards
- 2026-06-14 (overview figures + P1/P2 reduction reflected on the axiom surfaces)Research changelog; TFPT — Introduction and reading guide
Registered verification modules
No separate module is linked in this claim record. This is a coverage statement, not a verdict about its truth.
A registered module is a source reference. Its presence does not assert that the module was executed in this snapshot.