The hom-induced marking and its relator/frame facts #
The hom-induced marking: the generator values of a continuous hom
out of the candidate. Every weak-base object of this file is spelled at
THIS marking (one-spelling discipline; liftMarking is its framed-lift
restriction).
Equations
Instances For
Relators die at every hom-induced marking (GammaA_tameRel through
the finite-factor transport relator_eval_one_of_hom).
Relator operators are trivial at hom-induced markings (the
mChild_relator_tame_op_one input, with kernel membership replaced by
exact relator death).
The tame boundary relation at a hom-induced marking (the
mChild_tame_relation argument with the kernel input replaced by exact
relator death).
The x₀-slot of any Γ_A-framed marking is wild (the
mChild_marking_x0_mem_LY argument, made FramedPair-generic: the tame
boundary component of x₀ is trivial).
The density covering of the marking subgroup: when a continuous
hom out of Γ_A covers the target modulo a normal subgroup N, so does
the subgroup generated by its marking — the topological generation of
Γ_A pins the hom's range to the marking closure
(mChild_marking_covers freed from the framed-surjection packaging).
Realization of relator-killing framed markings #
The marked presentation's universal property, run at an arbitrary
marking whose relators die and whose wild slots land in L_Y — the
ExtensionStep construction with the base generalized from a framed
lift's perturbed marking to any marking (extImage/extMarking/extHom
mirrored verbatim; nothing here mentions a kernel).
The image subgroup of a marking.
Equations
Instances For
The corestricted marking of the image.
Equations
- Q2Presentation.Induction.markMarking q₀ a = ⟨q₀ a, ⋯⟩
Instances For
Relators transport into the corestricted marking.
Wild values in L_Y land in the image's 2-core.
Admissibility of a relator-killing wild-framed marking.
The realized hom: epi onto the marking image (the marked
presentation's universal property), included into Y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The realized hom takes the marking values on the generators.
The weak-base ledger dictionary #
weakZ1 E h ≃ ker (rowMap E q_h) at an arbitrary continuous hom h:
first cocycles ↔ homs congruent to h mod N (the liftHom_equiv_Z1
multiplication packaging), then homs ↔ row-kernel tuples (difference
rows one way, the marking realization the other).
The weak-lift carrier: continuous homs congruent to h modulo
the kernel (no surjectivity anywhere — the weak-base analogue of
liftHom's first clause).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The hom attached to a weak twisted cocycle: γ ↦ h γ · z γ (the
liftHom_equiv_Z1 packaging at a weak base).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cocycles are hom-differences at the weak base
(liftHom_equiv_Z1 with the framed base lift replaced by h).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel-valued difference tuple of a weak lift (the liftDiff
shape at the weak base).
Equations
- Q2Presentation.Induction.weakDiff E h F a = ⟨((ProfiniteGrp.Hom.hom h) (Q2Presentation.gammaGen a))⁻¹ * (ProfiniteGrp.Hom.hom ↑F) (Q2Presentation.gammaGen a), ⋯⟩
Instances For
A weak lift's marking is the base marking perturbed by the difference tuple.
The difference rows at the weak base: relators die at both
hom-induced markings, so the difference tuple kills both relator
shadows (liftDiff_rows with framed lifts replaced by weak lifts).
Perturbed-marking relator death: base death + zero shadow (the
perturb_eval_one argument at an arbitrary base marking).
Admissibility of the perturbed hom-induced marking at a row-satisfying tuple.
The weak extension step: a row-satisfying tuple over the
hom-induced marking realizes as a continuous hom with the perturbed
generator values (extLift's hom, base generalized to a marking).
Equations
- Q2Presentation.Induction.weakExtHom E h n hrowT hrowW hx0 hx1 = Q2Presentation.Induction.markHom (Q2Presentation.Lifting.perturb E (Q2Presentation.Induction.weakMarking h) n) ⋯
Instances For
The realized hom differs from the base by the tuple at each generator.
The realized hom is congruent to the base everywhere — density
pins the mod-N composites from their generator agreement (the
extLift lifting-clause argument at the weak base).
Weak lifts are row-kernel tuples — the ledger dictionary's
second half (liftHom_equiv_rowSystem/rowSystem_equiv_ker fused, at
the weak base).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weak-base ledger count: the twisted-cocycle set at an
arbitrary continuous hom has the cardinality of the row-map kernel at
the hom-induced marking (Z1_card_eq_ker_rowMap freed from the framed
base).
The computed-corank counting engine at a marking #
The (♦=) row-image identity and the rank–nullity count, marking-generic
(xr_rowMap_range_eq/xr_ker_rowMap_card with the kernel-compatible
marking hypotheses replaced by their consequences — the exact inputs a
hom-induced marking supplies).
(♦=) The row image at a relator-killing framed marking: exactly
the pairs whose sum is killed by every invariant dual — ⊆ by the rows
diagonal, ⊇ by the diamond image through the marked-window/
coannihilator identification.
The kernel count from the row-image identity — rank–nullity
against the sum-line size of the row image and the coannihilator
dimension count (xr_ker_rowMap_card's arithmetic, marking-generic):
|ker (rowMap)| = |N|²·|𝒳|, i.e. corank (rowMap) = dim 𝒳.
The candidate T'-count at every weak M-lift #
The fibre of a candidate weak M-lift covers B modulo M' (the
fibre_covers_mod_vLayer reading of the total-space clause, Γ_A
source, M-stage).
The candidate |Z¹(T')|-numeric at every weak M-lift (the
lem:affinelifting candidate T-stage factor of eq:mumultiplicity;
N5's weakZ1_tChild_card mirror): the ledger corank engine at the
child T'-kernel gives |Z¹_{A,f}(T')| = 2^{2·dimT + rT} at EVERY
total-space point — the corank of the row map is rT, the
prop:defduality instance at the T-layer.
The intrinsic bridge at candidate weak M-lifts (audit-§G1
discipline — PROVEN at total-space points from the fibre covering,
never assumed at weak bases): the g-intrinsic invariant duals at the
T'-kernel are the target-level ones (mapInvDuals_tChild_eq, Γ_A
source).
The candidate T'-count in the exact clause-(d) shape
|Z¹| = |N|²·|X_g| — the candidate prop:defduality instance at the
T-layer, division-free.
The btChild target numerics #
The 4 ∣ |B/T'| input of the diamond, mirrored from the child M-layer
argument (mChild_card_ne_two/mChild_card_Y_four) at the V-layer,
with the invariant-dual vanishing supplied by N5's vLayer_hinv.
The V-layer is nontrivial: |V| = 2^{dimV} > 1 from
head_nontrivial (the only place dimV ≥ 1 enters).
The V-layer never has exactly two elements: operators would be
trivial and a nonzero functional invariant, contradicting vLayer_hinv
(the mChild_card_ne_two argument one layer down).
4 divides |B/T'|: the V-layer is a 2-group of order
> 2 (the mChild_card_Y_four argument at btChild).
2 divides |B/T'|.
The candidate V-layer count at every V⋊C-lift #
The fibre of a candidate V-stage total-space point covers B/T'
modulo the V-layer (fibre_covers_mod_vLayer, Γ_A source).
The candidate |Z¹(V)|-numeric at every V⋊C-lift (the
lem:affinelifting candidate V-stage factor of eq:mumultiplicity;
N5's weakZ1_vLayer_card mirror): the same corank engine with
𝒳_V = ⊥ gives |Z¹_{A,f}(V)| = 2^{2·dimV} — the corank-0 face of
the ledger (the design's rT = 0 sanity anchor, realized at the
V-layer).
The intrinsic collapse at candidate V⋊C-lifts (audit-§G1
discipline; N5's mapInvDuals_vLayer_eq, Γ_A source).
At a candidate V⋊C-lift the intrinsic duals VANISH.
The candidate V-layer count in the exact clause-(d) shape
|Z¹| = |N|²·|X_g| — the candidate prop:defduality instance at the
V-layer.