A registered result in its source context
Original ledger classification: Formal [F] (uniformisation normal form) + [O] (the raw-seam marking obligation QGEO.MARKS.01)
Recorded statement: LEAN 4 FORMALISATION of QGEO.UNIFORM.01 (the geometric normal form of v177; the UNIFORM node of the QGEO proof tree) -- AUDIT: PASS, no sorry/admit, no domain axioms (only propext, Classical.choice, Quot.sound). New module…
Statement, assumptions and sources
Paper context: TFPT — Introduction and reading guide
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.QGEO.02
Original ledger classification: Formal [F] (uniformisation normal form) + [O] (the raw-seam marking obligation QGEO.MARKS.01)
Original claim text
LEAN 4 FORMALISATION of QGEO.UNIFORM.01 (the geometric normal form of v177; the UNIFORM node of the QGEO proof tree) -- AUDIT: PASS, no sorry/admit, no domain axioms (only propext, Classical.choice, Quot.sound). New module TfptCarrier/MobiusUniformisation.lean machine-proves the constructive uniformisation content: (1) [F] rho_pow_four: the clock rho:z->iz has rho^4=id; (2) [F] rho_order_exactly_four: rho^2 != id (rho^2(1)=-1), so the clock has order EXACTLY 4; (3) [F] sigma_invol: the reflection sigma:z->1/z is an involution; (4) [F] sigma_rho_sigma: sigma.rho.sigma = rho^{-1} (the dihedral relation => <rho,sigma>=D4 of order 8); (5) [F] orbit_scales_to_mu4: a non-fixed point a!=0 has orbit {a,ia,-a,-ia} that scales (z->z/a) exactly to mu4={1,i,-1,-i}; (6) [F] sigma_perm_mu4: sigma permutes mu4 (fixes 1,-1; swaps i,-i); (7) [F] mult_order_four_iff: a multiplier map z->zeta z has order exactly 4 (zeta^4=1, zeta^2!=1) IFF zeta=i or zeta=-i (the two primitive 4th roots; the inversion conjugates one to the other => canonical rep z->iz). Bundled as uniformisation_normal_form; signature-locked in AuditContract.lean. SCOPE: this is the constructive normal form GIVEN the four marks + clock (the [E] UNIFORM node); the RAW-seam obligation QGEO.MARKS.01 (the seam canonically producing a genus-0 four-marked D4 boundary) stays [O], NOT closed. Mirrors v177 (QGEO.UNIFORM.01); complements FORM.QGEO.01.
Original classification detail
Formal [F]/[O]: QGEO.UNIFORM.01 (order-4 Moebius normal form z->iz, D4 relation sigma.rho.sigma=rho^{-1}, orbit->mu4, multiplier classification zeta=+-i) Lean-proved (AUDIT: PASS, clean axioms, signature-locked); the raw-seam marking obligation QGEO.MARKS.01 stays [O]
Dependencies as recorded
QGEO.TREE.01; QGEO.MARKS.01; FORM.QGEO.01; FORM.GLUE.01
Open the original ledger source, row 297Location 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.
- Research contracts
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.
- Research Contract 1 — [formula in source]Research contracts
- Honest statusinput 4 origin theory
- Sharper still: one anchor [formula in source] , and [formula in source] as a compiler hull ( )TFPT — Introduction and reading guide
- Research Contract 1 — [formula in source]tfpt research contracts
- Honest statusorigin theory
- Honest statusOrigin Theory
- Honest statusinput 4 origin theory
- Front matter / supportFrontier and open physical interfaces
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.