A registered result in its source context

FORM.QGEO.03

Original ledger classification: Formal [F] (COHOM character grading + MODULE reflection parity) + [O] (the raw-seam obligations)

Original claim text

LEAN 4 FORMALISATION of QGEO.COHOM.01 (the character node of v177) + the MODULE reflection parity -- AUDIT: PASS, no sorry/admit, no domain axioms (only propext, Classical.choice, Quot.sound). New module TfptCarrier/CohomologyGrading.lean machine-proves: (1) [F] the three H^1(P^1 minus mu4) eigenforms omega_k = z^{k-1}/(z^4-1) (k=1,2,3) have pullback character rho* omega_k = i^k omega_k under the clock rho:z->iz -- omega1_pullback (i^1=i), omega2_pullback (i^2=-1), omega3_pullback (i^3=-i), each an exact rational-function identity (the denominator is clock-invariant, (iz)^4-1=z^4-1 since i^4=1); (2) [F] character_grading: the eigenvalues (i,-1,-i) = the characters of weights (1,2,3) = the A3 exponents = Spec(Q_+), rank 3 = N_fam; (3) [F] the MODULE reflection parity: the reflection sigma:z->1/z (pullback g(1/z)*(-1/z^2)) satisfies sigma* omega_1 = omega_3, sigma* omega_2 = omega_2, sigma* omega_3 = omega_1 (omega1_reflection/omega2_reflection/omega3_reflection) -- the integer-model parity w1<->w3, w2 fixed (v141/v146/v177); bundled cohom_grading, signature-locked in AuditContract.lean. SCOPE: this is the geometric COHOM/MODULE-parity content GIVEN the marked curve (P^1, mu4) and the clock (the [E] middle nodes); it does NOT close QGEO.MARKS.01/QGEO.KERNEL.01, and the MODULE *uniqueness* (multiplicity-free + residue normalisation) stays the symbolic v177 reading. Mirrors v177 (QGEO.COHOM.01); complements FORM.QGEO.01/02.

Original classification detail

Formal [F]/[O]: QGEO.COHOM.01 (pullback character rho* omega_k = i^k omega_k, grading (1,2,3)=A3 exponents) + MODULE reflection parity (sigma swaps omega1<->omega3, fixes omega2) Lean-proved (AUDIT: PASS, clean axioms, signature-locked); the MARKS/KERNEL obligations and MODULE uniqueness stay [O]

Dependencies as recorded

QGEO.TREE.01; QGEO.MARKS.01; FORM.QGEO.01; FORM.QGEO.02