11 VR-Transit
11.1 Position
VR-Transit is the tenth work of the cycle. It extends VR-Apparatus (Chapter 8) from “transit is well-behaved” (closed under composition and identity; Factorisable as the canonical Mode B witness) to two further statements: that transit is conservative over axioms, and that the leverage it provides takes the form of a bounded library of witnesses.
This is a clarity result, not new power. The apparatus does not extend what VR can prove. It contributes no axiom of its own to any transited object; it provides a conservative spine and an honest, bounded library of Factorisable bridges, and — the point of this chapter — it lets us say exactly where the axiom cost of a transit lives, and exactly where the witness method stops working. The universal form of conservativity is a meta statement about the kernel, exhibited on representatives, not proved as a single internal theorem (Section 11.2).
Two tracks, one of them out of reach. The apparatus has a predicate track and a reference track (Finding S3-A). The four providers of this chapter all live in the predicate track. The reference track was examined and yielded no clean witness method; structurally, non-descent there reduces to the need for Classical.choice, which cannot be witnessed (Finding TR-R1, Section 11.6). This is the sharpest result of the chapter.
11.2 Conservativity (I)
The apparatus is axiom-neutral: the internal carriers of conservativity are existing Axiom profile: [] lemmas, re-used, not re-proved.
The apparatus path from a witness to a Mode B operation, the transparency of the lift, and the composition of transits are all axiom-free. operand_determines_operational, factorisable_implies_isModeBOp, IsModeBOp_of_factorisable: Axiom profile: [] (the apparatus reductions). Factorisable.lift_val: Axiom profile: [], and it is rfl — the transited operation definitionally is the operation on the operational subtype (transparency). IsModeBOp.compose: Axiom profile: [] — composing two transits injects no axiom.
The universal form is meta. The statement “for all \(f\), \(\operatorname {axioms}(\operatorname {transit} f) = \operatorname {axioms}(f)\)” is a kernel-level fact: #print axioms is not an internal predicate one can quantify over. We therefore exhibit conservativity on representatives (Section 11.5), exactly as every chapter of the cycle already does with its axiom-audit footers, and prove only the schematic internal carriers above. No single universal internal theorem is claimed.
11.3 The four-source decomposition of cost
The central observation. Across the representative transited objects audited in Section 11.5, the axiom profile is exhibited as a decomposition into four named sources, with the apparatus contributing to none:
The operation source is itself a spectrum: algebraic infrastructure contributes [propext] (subgroup image), analytic operations contribute [propext, Classical.choice, Quot.sound] (Riesz); both are operation-side, neither is apparatus (Finding TR-C1). Aggregation over an explicit Finset contributes the choice-free [propext, Quot.sound]. Carrier encoding is an artefact: indexing by Fintype/Finset.univ inflates to the full ceiling, and is removable (Finding TR-FW1).
11.4 The witness library (II)
Leverage is a bounded library of Tier-2 domain-structure \(\to \) Factorisable bridges, each buying one family of transits. The bridges fall into two kinds, distinguished by their achievable axiom profile:
Pointwise bridges (target Axiom profile: []). Evaluate the witness at a single named operand; no summation.
HasFiniteGeneratorStructure \((T\, \iota )\) carries an axiom-free generator map gens : \(\iota \to T\) (Axiom profile: []). finiteGen_provides_factorisable: an operation agreeing with a globally operational \(g\) on every generator is Factorisable at each generator (Axiom profile: []). This mirrors separability_provides_factorisable with a finite index in place of a dense sequence.
For an operational normable functional \(f\) on an operational located subspace \(M \le E\), the located structure supplies the witness \(g := f \circ P_M\) (orthogonal projection), not merely the evaluation points. located_witness_operational: \(g\) is globally operational, re-using fn_computable_everywhere. located_provides_factorisable: any operation agreeing with \(g\) on the dense sequence is Factorisable there. Both Axiom profile: [propext, Classical.choice, Quot.sound] — faithful, source is the operation (projection via completeness), apparatus \(\varnothing \). This delivers the evaluation-point-level (Level B) Factorisable that Chapter 8 (separability) left deferred; the witness \(g = f\circ P_M\) is structural, distinct from the self-witnessing Riesz bridge — not a re-skin.
Aggregating bridge (target choice-free Axiom profile: [propext, Quot.sound]). Combining a witness over a finite operand set routes through Finset.sum; the achievable target is choice-free, not [].
finiteSpan_provides_factorisable: for additive maps agreeing on the generators, agreement propagates to every \(\mathbb {Z}\)-combination over an explicit Finset of indices, so the operation is Factorisable at any such combination (Axiom profile: [propext, Quot.sound]). This is the operand-not-operation principle (Finding S4-A) at the linear-combination level: the output’s operationality is fixed by the operand’s explicit coordinates, not by the map. Classical.choice is absent — finite additive transit is constructive.
The library thus spans density (separability, Chapter 8), completeness/projection (located), and finiteness (finite generators, in both a pointwise and an aggregating tier).
11.5 Axiom-attribution audit
The exhibited classification (file VRClassical/Transit/Conservativity.lean, which declares no public objects — it is an exhibition of existing profiles):
|
object |
profile |
source |
|
operand_determines_operational |
[] |
reduction |
|
factorisable_implies_isModeBOp |
[] |
reduction |
|
IsModeBOp_of_factorisable |
[] |
reduction |
|
Factorisable.lift_val |
[] |
transparency |
|
IsModeBOp.compose |
[] |
combinator |
|
separability_provides_factorisable |
[] |
pointwise |
|
finiteGen_provides_factorisable |
[] |
pointwise |
|
image_isOperationalAddSubgroup_isModeBOp |
[propext] |
operation/alg. |
|
finiteSpan_provides_factorisable |
[propext, Quot.sound] |
aggregation |
|
riesz_extension_isModeBOp |
[propext, Classical.choice, Quot.sound] |
operation/anal. |
The “apparatus” column is empty in every row. This table is the exhibited classification; it is not claimed as a single internal theorem. Gate verdict: thesis (I) holds on real cycle data.
11.6 Findings
Finding TR-R1 (headline): the witness method reaches exactly as far as the obstacle is witnessable. The four providers live in the predicate track, where the obstacle is concrete — density, projection, coordinates — and a witness can be exhibited. The reference track (setoids/quotients, \(\texttt{ZFSet} = \texttt{Quotient}\, \texttt{PSet.setoid}\)) was examined and yielded no clean witness method: a natural non-descending operation (selection) is not totally and purely expressible (one cannot extract an element of an arbitrary index type x.Type); the only total version uses Classical.choice, whose selection is opaque, so the defining non-descent is not even provable. Structurally, then, the reference track’s non-descending content coincides with the need for Classical.choice, and Classical.choice is precisely what cannot be witnessed. The operationalisation-by-witness method therefore works exactly where the obstruction is concrete and witnessable, and fails exactly where the obstruction is choice. This is a characterisation of the method’s reach, and it complements Finding S3-A from the Mode B side. The RefFactorisable abstraction is dropped (no nontrivial instance; recognition discipline).
Finding TR-FW1 (two faces, both removable; the A15 family). Finite additive transit cost lives in the carrier encoding, not the algebra. Face 1: indexing by Fin/Fintype and summing over Finset.univ inflates to [propext, Classical.choice, Quot.sound] — even a rfl identity carries it — whereas an explicit Finset keeps the sum choice-free. Face 2: a Finset field placed in the Tier-2 class contaminates the class type with [propext, Quot.sound] and the pointwise tier inherits it; keeping the class to its axiom-free generator map restores []. Rule canonised: axiom-bearing data belongs to the aggregating bridge’s arguments, never to a Tier-2 class shared with pointwise bridges.
Finding TR-C1: the operation source is a spectrum. image_isOperationalAddSubgroup_isModeBOp is [propext] (algebraic infrastructure), riesz_extension_isModeBOp is [propext, Classical.choice, Quot.sound] (analytic); both attribute to the operation, neither to the apparatus.
11.7 Honest scope
Predicate track only. The witness library and the exhibited conservativity are predicate-track results (Finding TR-R1).
Both extension candidates were examined and dropped, with reasons. An arithmetic/computability provider is redundant: IsComputableReal is already defined as carrying a rational algorithm with a convergence modulus, so a “modulus provider” restates the existing predicate, and the corpus deliberately does not use mathlib’s Computable (no Computable proofs for \(\mathbb {Q}\)-arithmetic); over \(\mathbb {N}\) the output predicate is trivial and the bridge collapses. A reference-track provider does not exist (Finding TR-R1). The ceiling has been probed from both sides; the spanning set is four predicate-track providers, not vapour.
Universal conservativity is meta. Exhibited on representatives, not an internal theorem (Section 11.2).
11.8 Position relative to existing work
The angle of VR-Transit — axiom attribution and transit conservativity as a lens — is distinct from proof mining (extracting bounds from classical proofs), reverse mathematics (calibrating theorems against subsystems), Bishop-style constructive analysis (rebuilding analysis without excluded middle), and computable analysis (representations and Type-2 effectivity). Chapter 8 already situates the cycle against these schools (its Remarks on related work); the delta here is only that VR-Transit measures the apparatus’s own axiom contribution (zero) and attributes each transit’s cost to a named source, rather than re-founding any mathematics.
11.9 References
The Lean 4 formalisation lives in the monorepo under VRClassical/Transit/ (modules FiniteWitness, Conservativity, Located) and is cited by GitHub tag on release, following the convention of VR-Algebra and VR-Topology. By curatorial decision there is no companion Zenodo record for this work; code is cited by tag, and this chapter is the canonical exposition. Findings are catalogued in T_FINDINGS_TRANSIT.md (TR-FW1, TR-C1, TR-R1).