Char-2 scalar helpers (private, decide-grounded) #
The coordinate surjectivity of the explicit limit model #
Mirror of piMon_surjective (Candidate/FiniteFactor.lean) at the explicit
model ProfiniteGrp.limit admissibleDiagram: the B-coordinate evaluation
is onto, because the universal generator family projects onto the marking
B.q, which generates by admissibility (map_evalAt_closure_eq_top).
The two-variable finite-coordinate factorization #
Pair mirror of the GREEN limit_finite_factor (Candidate/FiniteFactor.lean):
a continuous two-variable map from the explicit inverse-limit model to a
discrete space depends on a SINGLE coordinate in each variable. Fibres are
open; isOpen_prod_iff supplies a rectangle around each point; each side of
the rectangle contains a basic finite-coordinate box (isOpen_pi_iff);
compactness of the product extracts a finite subcover of two-sided boxes;
cofiltered domination (exists_dominating) collapses the union of all
mentioned coordinates to one index B.
Level descent of a locally constant 2-cochain on Γ_A #
Level descent (design §4-N4 step 1): a jointly locally constant
2-cochain on Γ_A factors through a single admissible coordinate
projection. Two-variable mirror of the GREEN GammaA_map_to_finite_factors
route: transport across gammaIso, apply limit_finite_factor_two, and
define the level cochain through chosen coordinate preimages
(limit_val_surjective).
The descended level cochain of a normalized continuous 2-cocycle is a
normalized 2-cocycle on the level carrier: the three laws descend through
the factorization along the SURJECTIVE piMon A
(piMon_surjective).
Common-level descent for a pair (design §4-N4 step 1, cofiltered
half): two normalized continuous 2-cocycles on Γ_A factor through ONE
admissible coordinate — factor each separately, dominate the two levels by
IsCofiltered.min, and transport along the transition maps (the
compatible-family identity m.2 f).
The level carrier: an admissible coordinate as a framed base #
levelBase A packages the admissible coordinate Fin A.n (spelled at the
diagram carrier ↥(admissibleDiagram.obj A), the house instance path) as a
BoundaryFramedTarget with marked wild kernel the 2-CORE — chosen so that
the pulled-back L_Y of any ζ-cocycle cover contains the canonical marking
of the two wild generators (A.admissible's 2-core clauses), which is what
anyMarking_admissible needs. This is PRIVATE SCAFFOLDING for the token
proof; no downstream unit consumes it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tame relator dies at the level marking A.q (spelled at the level
carrier — the coordinatewise relation GammaA_tameRel rewritten through
gammaGen_eval_projection, so no cross-carrier exact is needed).
The wild relator dies at the level marking A.q.
The canonical (zero-scalar) marking of the ζ-cover extension over the
level base: a ↦ (A.q a, 0).
Equations
- Q2Presentation.Induction.levelMarking A zeta hz1 hz2 hzc a = { base := A.q a, scal := 0 }
Instances For
The candidate level trace ι_A(ζ) (the prop:chainmap trace,
l.1687): the sum of the scalar reads of the two marked relators, evaluated
in the ζ-extension at the canonical marking. levelTrace_eq_of_base shows
it is marking-independent; cochainSolvable_iff_levelTrace_eq_zero shows it
is THE solvability functional.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Definitional form of levelTrace (the P7 _def rfl-lemma fix-class).
Pushing a base-compatible marking through the deck projection kills any
relator that dies at A.q (via GExpr.eval_map along cocycleProj).
Multiplying by a deck-kernel element shifts the scalar read additively
(the base slot of the kernel factor is 1, and ζ(·, 1) = 0).
K1 — marking independence of the trace (design §4-N4: "the affine
solvability locus is a hyperplane"): every base-compatible marking reads the
SAME trace as the canonical one. Compatible markings differ by a
deck-kernel perturbation (compat_eq_perturb); the perturbation shifts the
two relator reads by the two row-map slots, which COINCIDE at an order-2
kernel (rowMap_card_two_apply: both are the τ-slot), so char-2 cancels
the shift in the trace.
The deck projection of the ζ-cover, as a hom of (finite discrete)
profinite groups into the level coordinate (the cocycleCollapseHom
idiom).
Equations
- One or more equations did not get rendered due to their size.
Instances For
K2, forward half — zero trace gives a continuous solution (design
§4-N4: "(both reads correctable)" at the diagonal image): if the level
trace vanishes, the two relator defects of the canonical marking are EQUAL
kernel elements, so the constant τ-slot variation kills both
(rowMap_card_two_apply + the exponent-2 law). The corrected marking is
admissible on its image (anyMarking_admissible — the wild generators land
in the pulled-back 2-core), anyHom produces the continuous hom out of
Γ_A, its base component agrees with π_A on the topological generators
(homs_ext_on_gen), and its scalar component solves the pulled-back
equation.
The graph hom of a solving cochain: γ ↦ (π_A γ, c γ) is a
continuous hom into the ζ-extension (the N2 assembly idiom of
cocycleCoverLiftHom_iff_cochainSolvable, backward direction, with base
component the coordinate projection).
Equations
- One or more equations did not get rendered due to their size.
Instances For
K2, backward half — solvability forces zero trace: a solving cochain
graphs to a continuous hom into the extension; both relators die along any
hom out of Γ_A (tameRelator_eval_one_of_hom / wildRelator_...), so the
graph marking has trace 0; by K1 so does the canonical one.
K2 — the trace is the solvability functional (the falsifiable
instrument: per descended (A, ζ), solvability of the pulled-back equation
on Γ_A is ONE finite 𝔽₂-computation).
Trace additivity (K3): the prop:chainmap trace linearity #
Evaluation is pushed through the base-fibre product of two ζ-extensions and
the scalar-sum hom — pure GExpr.eval_map functoriality, no word
induction (the ω₂-powers ride along because powOmega2 commutes with all
finite-group homs, map_powOmega2).
The base-fibre product of the two ζ-extensions: pairs with EQUAL base components, as a subgroup of the direct product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scalar-sum hom out of the base-fibre product into the
(ζ₁ + ζ₂)-extension: ((y, s), (y, t)) ↦ (y, s + t). Multiplicativity
is EXACTLY the pointwise sum of the two cocycle laws at matching bases.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diagonal canonical marking of the base-fibre product.
Equations
Instances For
K3 — trace additivity in the cocycle (prop:chainmap's
D²(u_t, u_w) = u_t + u_w read as linearity of the two relator scalars):
the trace of a pointwise sum of level cocycles is the sum of the traces.
Proof: evaluate the two relators once in the base-fibre product at the
diagonal marking, and push through the three homs (two projections, one
scalar-sum) by GExpr.eval_map.
The candidate ι-token #
The candidate ι-additivity token is a THEOREM (design §4-N4 target;
floor F-ι-cand sec7_candidate_iotaToken DISSOLVED at birth — stated with
the design's floor name so N7 consumers cite one name on both sources,
mirroring the citable q2_trivialCoeff_h2_line : IotaToken GQ2Profinite).
dim H²(Γ_A, 𝔽₂) ≤ 1 in the solvability spelling: two unsolvable
normalized continuous 2-cocycle equations on the candidate source have
solvable sum. Manuscript content: prop:chainmap (l.1687) +
lem:finitewordstokes — realized through the ledger: descend both
equations to a common admissible level (gammaA_cochain_factors_pair),
where solvability is the vanishing of the relator-read TRACE
(cochainSolvable_iff_levelTrace_eq_zero; the variation image at the
order-2 deck kernel is the diagonal, rowMap_card_two_apply — codimension
EXACTLY 1, the Phase-2 gate of the design); the trace is additive
(levelTrace_add), and 1 + 1 = 0 in 𝔽₂.
Consumer hooks (the design's "vanishing spec the phase bridge needs") #
N7/N9 consume the token only through the N2 readings; the two corollaries
below pre-instantiate them at the candidate source so the engine files can
cite Γ_A-additivity without touching the token.
iotaRead at the candidate source is additive on normalized continuous
2-cocycle pairs.
The ±1-indicator at the candidate source is multiplicative on
normalized continuous 2-cocycle pairs.