Shapiro ledger: Lemma 6.15 free (104) and involution (105)

Proves the two non-on-the-nose orbit cases of the paper's Lemma 6.15 (the square case (103) is already proved on the nose in GQ2/SectionSix.lean). The ĝ-shift changes the canonical transversal representatives (Quotient.out) by right-N corrections; the two raw cochains (graph pullback vs. corestriction) therefore differ by a coboundary, not literally.

The engine:

• smul_zmodTwo — every DistribMulAction _ (ZMod 2) is trivial (Aut(𝔽₂) = 1), so a Z¹(N, 𝔽₂) cocycle is a genuine homomorphism N → 𝔽₂ (z1_mul/z1_one/z1_inv).
• H2ofFun_eq_of_sub_mem_B2 — if φ − ψ ∈ B² then H2ofFun φ = H2ofFun ψ (junk-total, so this is all that is needed: it forces φ ∈ Z² ↔ ψ ∈ Z² and equal classes when both hold).
• lWord_mul — the transversal 1-cochain is a cocycle: ℓ_h(γη) = ℓ_h(γ)·ℓ_{γ̄⁻¹h}(η).
• shiftCorr / lWord_shift — the .out discrepancy ℓ_{kḡ}(η) = c(k)⁻¹·(ĝ⁻¹ℓ_k(η)ĝ)·c(η̄⁻¹k).

For the free case, these combine (with a finsum reindex over G/N and the ℓ-cocycle identity) to give φ − ψ = δ¹Λ for the explicit 1-cochain Λ(γ) = Σ_h α(ℓ_h(γ))·β(c(γ̄⁻¹h)) (lemma_6_15_free_aux, proved, std-3).

Paper: Lemma 6.15, eqs. (104)/(105), proof pp. 31–32 (the (106)/(108) bar-corestriction identities). No axioms (Ax = ∅).

Proof architecture

• lemma_6_15_free_aux proves the free-orbit case by reindexing the corestriction sum and exhibiting the explicit coboundary δ¹Λ.
• For involution orbits, invIndexEquiv : G/U₀ ≃ (G/N)/⟨ḡ⟩ aligns the two index sets, while lWordU0_factor, alpha_lWordU0_aligned, and alpha_lWordU0_flipped express the transversal discrepancy through explicit N-corrections. The bS and evensAux decompositions then assemble the required coboundary.
• lemma_6_15_involution_aux combines the compatible-transversal and transversal-change coboundaries to prove the involution-orbit identity in H².

Import architecture

The factor-set / orbit-data def-layer (FactorSet, graphPullback, RegRep, *OrbitDatum, …) now lives in GQ2/OrbitData.lean (top-level namespace GQ2); this file imports that (not SectionSix), so SectionSix can import ShapiroLedger and splice lemma_6_15_free := ShapiroLedger.lemma_6_15_free_aux N hNo α β ghat with no import cycle (SectionSix → ShapiroLedger → OrbitData, and SectionSix → OrbitData). That splice is now live for both the free and involution cases. See docs/orchestration/orbit-data-refactor.md for the reason the factor-set definitions live in their own module.

File organisation. The ledger is split into Free (the general transversal and free-orbit machinery) and Involution (the compatible-transversal involution calculation). This umbrella preserves the original import path and public declaration names.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (104) = ⟦eq-shapirofree⟧
• eq. (107) = ⟦eq-halfgraph-explicit⟧
• eq. (67) = ⟦eq-piepsilon⟧
• Lemma 6.15 = ⟦lem-orbitshapiro⟧