AxiomAudit.lean

/-
# Axiom audit — the checked public-surface inventory

A standalone build target, deliberately outside the `LogicalInduction` library: the
library carries the mathematics, this target carries the check. Anything *not* listed here
is internal and may be renamed, moved, or inlined freely; changes to a listed statement are
surface changes and must be flagged.

**Two kinds of listing, and they are not the same claim.** In the `LogicalInduction`
section:

  * the **public canonical endpoint inventory** — the block delimited by
    `LI-CANONICAL-BEGIN` / `LI-CANONICAL-END`, which names exactly the endpoints of
    `scripts/coverage-classification.md`'s *endpoints* table. This is the table of contents
    for the human statement read-through, and it is what `docs/trust-surface.html` renders
    with full signatures.
  * **internal axiom regression assertions** — every other `#assert_axioms_clean` block.
    These are under the build gate and stay there; they are construction machinery,
    compatibility carriers and supporting lemmas, not the public read-through set. Wanting a
    regression guard on a declaration is not a reason to publish it.

Carrying a `Paper node:` label is a third, weaker thing again: it is *provenance*, not
publication. `thm:scon` has 54 axiom-checked carriers and 4 canonical endpoints. The other
50 are real, checked, and deliberately not shown.

`scripts/check_endpoint_coverage.py` enforces that the canonical block and the endpoints
table name exactly the same declarations, so the three artifacts cannot drift apart the way
they had by 2026-08.

The build fails if any listed endpoint acquires an axiom beyond `propext`,
`Classical.choice`, `Quot.sound` (in particular `sorryAx`), or ceases to exist.

Two independent claims, checked separately — do not conflate them:
  * **axiom cleanliness** (this build): every *listed* endpoint is `sorry`-free and uses no
    stray axioms. It says nothing about whether the list is complete.
  * **surface completeness** (`scripts/check_endpoint_coverage.py`): every paper `\label`
    cited in a `Paper node:` annotation has at least one endpoint *in this list*. It says
    nothing about axioms, nor about whether the listed endpoint is the strongest form of
    the theorem (that is the human statement read-through's job — see below).
Green here + green there = "the enumerated surface is clean and covers every annotated
paper node", not "the formalization is faithful". Faithfulness is the read-through.

Scope is the whole repository, and it is now **strictly clean throughout**: the former
sole intentional axiom `glFixedPoint_thm42` (GL fixed-point existence) has been discharged
by the `ProvabilityLogic/` development (a vendored subset of
FormalizedFormalLogic/ProvabilityLogic, pinned in `lakefile.lean`; see
`ModalAgents/FixedPoint.lean`),
so every ModalAgents endpoint — including the cooperation results that rest on the GL fixed
point — is asserted under `#assert_axioms_clean`. (`#assert_axioms_clean_except` is retained
as a reusable tool but is no longer needed.)

## Tier-2 membership, annotations, and regeneration

**Tier 2 (`#assert_fields`)** freezes boundary *structures*: a structure's fields are
the hypotheses its endpoints consume, so adding or removing one is premise smuggling.
Membership is mechanical, not taste: a structure is Tier 2 iff it appears in the type
of a Tier-1 endpoint, transitively through structure fields — computed by
`SurfaceProbe.lean`'s `#surface_types`. Transitive closure is the right depth because
reading an endpoint means understanding every structure its hypotheses mention.

**Annotation convention**: the last line of every inventory member's docstring is
`Paper node: ` followed by backticked labels taken verbatim from `\label{…}` in
`LogicalInduction/notes/1609.03543v5-main.tex`, comma-separated — no ranges, no glosses, so every label
is greppable. Members realizing the efficient-computability obligation without a node
of their own carry `def:ec`; graded-strength endpoints share their theorem's node.

**Regeneration** after a deliberate surface change: rerun `#surface_types` (seeded
with the current `#assert_axioms_clean` names) and `#dump_fields` in
`SurfaceProbe.lean`, update the `#assert_fields` block and affected `Paper node:`
fields here, then run `scripts/check-paper-nodes.sh`.
-/
import Lean.Util.CollectAxioms
import LogicalInduction.Properties
import LogicalInduction.Construction
import LogicalInduction.API
import ModalAgents.Cooperation
import ModalAgents.Behavioral
import ModalAgents.FixedPoint
import ModalAgents.Arithmetic
import ModalAgents.ArithmeticAgent
import CartesianFrames.Examples
import CartesianFrames.Worlds
import CartesianFrames.Subagent
import CartesianFrames.AdditiveMultiplicative
import CartesianFrames.Operations
import CartesianFrames.Categorical
import FiniteFactoredSets
import Condensation
import FactoredSpaces

open Lean Elab Command in
/-- Fail elaboration unless every named declaration exists and depends on no axioms
beyond `propext`, `Classical.choice`, and `Quot.sound`. -/
elab "#assert_axioms_clean " ids:ident+ : command => do
  for id in ids do
    let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
    let axioms ← Lean.collectAxioms name
    let bad := axioms.filter (! [``propext, ``Classical.choice, ``Quot.sound].contains ·)
    unless bad.isEmpty do
      throwErrorAt id "'{name}' depends on disallowed axioms: {bad.toList}"

open Lean Elab Command in
/-- Like `#assert_axioms_clean`, but additionally permits the one named axiom `extra`
(for the intentionally axiomatized `ModalAgents/` fixed-point fact). Still fails on `sorryAx`
or any other axiom. -/
elab "#assert_axioms_clean_except " extra:ident ids:ident+ : command => do
  let extraName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo extra
  for id in ids do
    let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
    let axioms ← Lean.collectAxioms name
    let allowed := [``propext, ``Classical.choice, ``Quot.sound, extraName]
    let bad := axioms.filter (! allowed.contains ·)
    unless bad.isEmpty do
      throwErrorAt id "'{name}' depends on disallowed axioms: {bad.toList}"

open Lean Elab Command in
/-- Fail elaboration unless `struct` is a structure whose field-name set is exactly the
listed idents. Freezes the field *names* of a boundary structure — adding or removing a
field fails the build — but NOT their types: a field's type can change without failing
this check (it has, benignly: `mesh_poly`'s index moved during the precision reindex).
A type change on a frozen structure is still a surface change and must be flagged in a
comment here, as the `BitPrefixSentences.prefix_codes` note below does. Order-insensitive. -/
elab "#assert_fields " struct:ident fields:ident* : command => do
  let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo struct
  unless Lean.isStructure (← getEnv) name do
    throwErrorAt struct "'{name}' is not a structure"
  let actual := ((Lean.getStructureFields (← getEnv) name).map (·.toString)).qsort (· < ·)
  let expected := (fields.map (·.getId.toString)).qsort (· < ·)
  unless actual.toList == expected.toList do
    throwErrorAt struct
      "'{name}' fields changed.\n  expected: {expected.toList}\n  actual:   {actual.toList}"

namespace LogicalInduction

open ConditioningCompile FeedbackTruth FeedbackEmission PrefixPatchCompile

/-! ## Public canonical endpoint inventory

**This block is the trust surface a reader is asked to read.** It names exactly the
canonical endpoints of `scripts/coverage-classification.md`'s *endpoints* table — the
declarations `docs/trust-surface.html` renders with full signatures, one small curated set
per paper node, the paper's own printed form first.

Every *other* `#assert_axioms_clean` block below is an **internal axiom regression
assertion**: still under the build gate, so nothing lost its guard and build coverage is
unchanged, but not public trust surface. Being worth freezing is not a reason to put a
declaration in front of a reader. `thm:scon` has 54 axiom-checked carriers and 4 canonical
endpoints; `def:ec` has 24 and 3.

The delimiters are machine-read: `scripts/check_endpoint_coverage.py` fails the run unless
the name set here equals the endpoints table's, spelling included — so the two cannot drift,
and a curated node cannot silently fall back to an arbitrary carrier (which is exactly what
happened to `thm:ifp`, whose refutation and corrected theorem were both invisible).

Names are repeated from the topical blocks below on purpose: this list is a *view*, and the
topical blocks stay the place where each endpoint is explained. -/

-- LI-CANONICAL-BEGIN
#assert_axioms_clean
  AffineCombination AffineCombination.BoundedCombinationSequence LUVCombination.BoundedSequence
  PaperLUVCombination.boundedSequence unitFracPaperLUVBoundedSequence DeductiveProcess
  DeductiveProcessComputation DeferralFunction MachineEfficientTrader EfficientlyComputable
  EfficientlyComputable.toMachine GeneratedRatFeature PGenerableWeighting liaStates liaHistory
  IsMachineLogicalInductor IsLogicalInductor PaperLUV LUV unitFracPaperLUVSeq Trader Strategy
  LUVCombination.BoundedSequence.mesh_independence_ofSyntax trading_firm_dominance
  AffineCombination.PolySequence.affcoh AffineCombination.BoundedCombinationSequence.affpolymax
  AffineCombination.PolySequence.affine_provind_theory_ge
  AffineCombination.PolySequence.affine_provind_theory_le
  AffineCombination.PolySequence.affine_provind_theory_eq lic_learning_pseudorandom_frequency
  lic_learning_pseudorandom_frequency_above lic_learning_pseudorandom_frequency_below
  lic_no_expected_net_update_conditional_paperLUV_closed
  lic_no_expected_net_update_conditional_exact_canonical lic_expected_future_expectations_closed
  lic_no_expected_net_update_closed lic_limitingBelief_tendsto lic_price_convergesTo
  lic_does_not_anticipate_halting_unconditional
  lic_domination_universalSemimeasure_ofIndependentAtoms lic_domination_universalSemimeasure
  LUV.expect_converges lic_expectation_indicator lic_expectations_of_probabilities_closed
  lic_iterated_expectations_closed LUVCombination.BoundedSequence.expcoh_ofSyntax
  LUVCombination.BoundedSequence.exppolymax_ofSyntax lic_expect_combination_provind_ge
  lic_expect_combination_provind_le lic_expect_combination_provind_eq
  lia_learns_halting_patterns_unconditional
  FinitePerturbationCounterexample.not_overgeneral_ifp
  FreezeOracle.machine_lic_iff_of_finiteSupport
  LIAPerturbation.machineLogicalInductor_liaPerturbed
  lic_disbelief_inconsistent_theories_unconditional lic_limitCoherence
  lic_learning_exclusive_exhaustive exists_computable_beliefSequence_logical_inductor
  exists_machine_logical_inductor LIA_isMachineLogicalInductor LIA_is_logical_inductor
  lic_linearity_of_expectation_seq lic_learns_provable_nonhalting_patterns_unconditional
  lic_paradox_resistance_ofDiagonal_unconditional lic_nonDogmatism lic_nonDogmatism_dual
  UPrefix.lic_occamBounds_ofUniversalPrefix lic_uniform_nonDogmatism_ofCE
  lic_uniform_nonDogmatism lic_belief_finitistic_consistency_unconditional
  lic_belief_stronger_theory_consistency_unconditional AffineCombination.PolySequence.peraffkno
  LUVCombination.BoundedSequence.perexpkno_ofSyntax lic_persistence_of_knowledge
  lic_learning_varied_pseudorandom lic_learning_varied_pseudorandom_above
  lic_learning_varied_pseudorandom_below
  AffineCombination.BoundedCombinationSequence.prandaff_above
  AffineCombination.BoundedCombinationSequence.prandaff_below
  AffineCombination.BoundedCombinationSequence.prandaff LUVCombination.BoundedSequence.prandexp
  LUVCombination.BoundedSequence.prandexp_below LUVCombination.BoundedSequence.prandexp_eq
  lic_provind AffineCombination.BoundedCombinationSequence.recunbiasedaff
  AffineCombination.recurringunbiasedness
  LUVCombination.BoundedSequence.recurringunbiasednessexp lic_introspection_closed
  lic_introspection ConditioningCompile.lic_conditioned_fixed_machine
  ConditioningCompile.lic_conditioned_growing_machine_ofProcessComputation
  ConditioningCompile.lic_conditioned_growing_machine_ofSequence
  lic_conditioned_fixed_machine_unconditional lic_conditioned_growing_machine_unconditional
  AffineCombination.simcal AffineCombination.sentenceAffine_polySequence
  calibrationIndicator_pgenerable lic_self_trust_closed
  lic_strict_domination_universalSemimeasure_ofAtomCodes
  lic_strict_domination_universalSemimeasure lic_preemptive_learning
  FeedbackTruth.lic_wub_ofComputation FeedbackTruth.lic_wub_ofComputation_unconditional
  FeedbackTruth.boundedCombination_wubaff_ofComputation
  FeedbackTruth.boundedCombination_wubaff_ofComputation_unconditional
  FeedbackTruth.luv_wubexp_ofComputation FeedbackTruth.luv_wubexp_ofComputation_unconditional
-- LI-CANONICAL-END

/-! ## Existence (`thm:li`) -/

#assert_axioms_clean exists_logical_inductor LIA_is_logical_inductor
  exists_computable_beliefSequence_logical_inductor
  exists_machine_logical_inductor LIA_isMachineLogicalInductor

-- The canonical trader universe is `MachineEfficientTrader` — ordinary machine
-- polynomial time, through `Complexity.FP`. The enumeration is sound and covers the whole
-- class, and the fuel calculus's certificates land inside it.
#assert_axioms_clean
  trading_firm_dominance exists_enumeratedTrader_eq enumeratedTrader_machineEfficient
  enumeratedOutput_mem_FP EfficientlyComputable.toMachine
  lia_no_machine_trader_exploits

/-! ## Property tail, conditional on `[IsLogicalInductor P DP]` -/

-- Properties/Coherence.lean
#assert_axioms_clean
  lic_disprovable_tendsto_zero lic_excl_gap_tendsto_zero lic_limit_additive
  lic_price_convergesTo

-- Properties/LimitCoherence.lean
#assert_axioms_clean lic_limitCoherence

-- Properties/ProvabilityInduction.lean, Properties/AffineCoherence.lean
-- Tier note: `lic_provind` / `lic_provind_true` / `lic_provind_false` are the
-- paper-facing `thm:provind` (theorems may appear arbitrarily late in the process).
-- `lic_deducible_*` and `lic_provind_seq` are retained FRAGMENTS whose membership
-- hypotheses (`φ ∈ D n` at every / its own index) are stronger than the paper's —
-- do not credit them as `thm:provind`.
#assert_axioms_clean
  lic_deducible_eventually_ge lic_deducible_price_near_one lic_deducible_tendsto_one
  lic_provind_seq lic_provind lic_provind_true lic_provind_false

-- Properties/TimelyLearning.lean, Properties/AffinePersistence.lean
#assert_axioms_clean
  lic_preemptive_learning lic_persistence_of_knowledge lic_persistence_of_knowledge_lower
  lic_persistence_of_knowledge_upper lic_centered_persistence lic_limitingBelief_tendsto

-- Properties/AffineCoherence.lean, AffinePreemptiveLearning.lean, AffinePersistence.lean:
-- the paper-facing analytic affine capstones (`thm:affcoh`, `thm:affpolymax`, `thm:peraffkno`)
-- and all three comparison forms of `thm:affprovind`.
-- Tier note: `thm:affprovind` is the affine statement — a bounded combination sequence and a
-- real bound `b`, in `≥`/`≤`/`=` forms.  It is these three, NOT `lic_provind_true`/`_false`,
-- which are the sentence-level halves of `thm:provind` (the `k=1`, `b ∈ {0,1}` special case).
#assert_axioms_clean
  AffineCombination.PolySequence.affcoh
  AffineCombination.BoundedCombinationSequence.affpolymax
  AffineCombination.PolySequence.peraffkno
  AffineCombination.PolySequence.affine_provind_theory_ge
  AffineCombination.PolySequence.affine_provind_theory_le
  AffineCombination.PolySequence.affine_provind_theory_eq

-- Properties/NonDogmatism.lean, Properties/UniformNonDogmatism.lean
-- Tier note: `lic_nonDogmatism` / `lic_nonDogmatism_dual` are the paper-facing `thm:nd`;
-- `lic_nonDogmatism_weak` is a retained FRAGMENT (its lower bound decays with `n`).
#assert_axioms_clean
  lic_nonDogmatism lic_nonDogmatism_dual lic_nonDogmatism_weak lic_limit_pos
  lic_limit_lt_one lic_uniform_nonDogmatism lic_uniform_nonDogmatism_repeating

-- Properties/OccamBounds.lean, Properties/UniversalSemimeasure.lean
#assert_axioms_clean
  lic_occamBounds lic_occam_lower lic_limitingBelief_add_neg
  lic_domination_universalSemimeasure lic_strict_domination_universalSemimeasure

-- Construction/Witnesses/KraftInequality.lean — the Kraft inequality underlying the
-- prefix-machine complexity bounds.  Proof body autoformalized by Aristotle and
-- kernel-revalidated in-repo; the statement is audited surface, the generated interior
-- has not had a line-by-line human read.
#assert_axioms_clean
  kraft_inequality

-- Construction/Witnesses/PrefixMachine.lean — the concrete self-delimiting sentence code,
-- with both fuel-model emission certificates constructed (no operational input remains).
#assert_axioms_clean
  prefixKraft prefixNegationCompiler
  invalidBit_polyFueled prefixSentenceEnum_polySentenceCodes prefixApprox_polyRatCodes
  lic_occam_lower_ofPrefixMachine lic_occamBounds_ofPrefixMachine

-- Construction/Witnesses/UniversalPrefix.lean (the self-delimiting UNIVERSAL prefix
-- machine).  `dom U` is prefix-free by construction, so the Kraft field
-- needs no hypothesis; `kappaU_le_of_prefixMachine` is the invariance theorem that earns
-- the word "universal"; `uSel_polyRatCodes` builds the polynomial clock (a self-clamped
-- `evaln` selection) on top of the exact stage table, whose own program
-- `uCode` is now CONSTRUCTED (`exists_uCode`, via the bounded search `uMinLen`), so the
-- two endpoints carry no operational input at all.
#assert_axioms_clean
  UPrefix.UHalt_prefixFree UPrefix.UHalt_functional UPrefix.acc_antichain
  UPrefix.kappaU_kraft UPrefix.kappaUNegationCompiler
  UPrefix.kappaU_le_of_prefixMachine UPrefix.kappaStage_eventually_eq
  UPrefix.uMinLen_eq UPrefix.uEmit_prim UPrefix.exists_uCode
  UPrefix.uSel_polyRatCodes UPrefix.universalPrefixPresentation
  UPrefix.universalPrefixThresholdEmission
  UPrefix.lic_occam_lower_ofUniversalPrefix UPrefix.lic_occamBounds_ofUniversalPrefix

-- Properties/Conditioning.lean, Properties/FinitePerturbations.lean
-- Tier note: `isLogicalInductor_of_stage_unsatisfiable` (Framework/Affine.lean) is the
-- degenerate half of `thm:scon` — the criterion over a deductive process one of whose
-- stages has no propositionally consistent world.  It is listed here because it is what
-- lets the `thm:scon` endpoints drop the repo-side joint-consistency hypothesis and match
-- the paper's premise-free statement.  For the growing form the other half of that split is
-- `DeductiveProcess.exists_consistentWithTheory` (Framework/Compactness.lean): propositional
-- compactness over Cantor space, which converts per-stage satisfiability of the union
-- process into the single world the price-floor argument consumes.  It is internal
-- infrastructure, not a paper node, so it is not itself an inventory member; its axiom
-- report is covered transitively by the `thm:scon` endpoints below.
#assert_axioms_clean
  lic_conditioned lic_conditioned_gated lic_conditioned_eventual
  lic_conditioned_machine lic_conditioned_gated_machine lic_conditioned_eventual_machine
  isLogicalInductor_of_stage_unsatisfiable
  isMachineLogicalInductor_of_stage_unsatisfiable
  lic_iff_of_finitePerturbation
  lic_iff_of_finiteSupportPerturbation machine_lic_iff_of_finiteSupportPerturbation

-- Construction/Witnesses/FinitePerturbationWitness.lean — the REFUTATION of `thm:ifp`.
-- The paper's printed statement is false; `not_overgeneral_ifp` proves its negation at the
-- paper's own quantifier, with no theory parameter (`_ofTheory` is the same over any Σ₁-sound
-- Δ₁ theory extending `𝗜𝚺₁`), from the constructed `LIA` and a day-`0` advice tape.  It is a
-- canonical endpoint — the reader of `thm:ifp` must meet it first — and is therefore in the
-- LI-CANONICAL block above as well; the three carriers listed immediately above are the
-- compatibility renderings of the CORRECTED statement and are internal, two of them with
-- patch hypotheses that are uninhabited (see the RpnFreeze note below).  `notes/paper-errata.md`
-- PE1 is the ledger.
#assert_axioms_clean
  FinitePerturbationCounterexample.not_overgeneral_ifp

-- Properties/Pseudorandomness.lean
#assert_axioms_clean
  lic_learning_pseudorandom_frequency lic_learning_pseudorandom_frequency_above
  lic_learning_pseudorandom_frequency_below lic_learning_varied_pseudorandom
  lic_learning_varied_pseudorandom_above lic_learning_varied_pseudorandom_below
  AffineCombination.BoundedCombinationSequence.recunbiasedaff
  AffineCombination.BoundedCombinationSequence.prandaff
  AffineCombination.BoundedCombinationSequence.prandaff_above
  AffineCombination.BoundedCombinationSequence.prandaff_below
  AffineCombination.recurringunbiasedness AffineCombination.simcal
  AffineCombination.lic_not_frequently_positive_feedback_return
  AffineCombination.lic_wub AffineCombination.lic_wubaff

-- Properties/Relationships.lean
#assert_axioms_clean
  lic_imp_eventually_le lic_lex_tendsto_zero lic_learning_exclusive_exhaustive

-- Properties/ExpectationAffine.lean, Properties/Introspection.lean,
-- Properties/SelfTrust.lean
#assert_axioms_clean
  lic_linearity_of_expectation lic_expectation_indicator lic_expectation_provind
  lic_linearity_of_expectation_ofValuesAt lic_expectation_provind_ofValuesAt
  lic_expectation_provind_le lic_expectation_provind_eq
  lic_expect_combination_provind_zero lic_expect_combination_provind_le_ofDetermined
  lic_expect_combination_provind_ge_ofDetermined lic_expect_combination_provind_eq_ofDetermined
  lic_expect_combination_provind_le
  lic_expect_combination_provind_ge
  lic_expect_combination_provind_eq
  lic_linearity_of_expectation_seq
  lic_introspection lic_paradox_resistance lic_expectations_of_probabilities
  lic_iterated_expectations lic_self_trust lic_expected_future_expectations

-- Properties/ExpectationConvergence.lean: Expectations Converge (`thm:ec`).
#assert_axioms_clean LUV.expect_converges

-- Properties/ExpectationProperties.lean: the paper-facing LUV-combination sequence
-- capstones (`thm:exppolymax`, `thm:expcoh`, `thm:perexpkno`, `thm:wubexp`).
#assert_axioms_clean
  LUVCombination.BoundedSequence.mesh_independence
  LUVCombination.BoundedSequence.exppolymax
  LUVCombination.BoundedSequence.expcoh
  LUVCombination.BoundedSequence.perexpkno
  LUVCombination.BoundedSequence.wubexp

-- Construction/Witnesses/LUVExpectationCertified.lean (`dd:luv-arith`): the
-- expectation endpoints whose world-value hypotheses are discharged from arithmetic
-- (`thm:loe`, `thm:expprovind`).  The certified LUV, its derived world-value
-- interfaces (`threshold_holds_iff`, `exactTheoryPresentation_ofArithmetic`), and the
-- process realizing them (`luvArithmeticPresentation`) are internal infrastructure.
#assert_axioms_clean
  ComputableLUV.lic_expectation_provind_arith
  ComputableLUV.lic_expectation_provind_le_arith
  ComputableLUV.lic_expectation_provind_eq_arith
  ComputableLUV.lic_linearity_of_expectation_arith
  ComputableLUV.exppolymax_arith ComputableLUV.wubexp_arith
  ComputableLUV.expcoh_arith ComputableLUV.perexpkno_arith

-- dd:fuel model card (`def:ec`): the fuel certificate's own trust facts — poly-fueled ⟹
-- primrec, the runtime-gcd inhabitation witness, the size-based separation (2^n is not
-- poly-fueled), and the two-sided EF.cost ↔ token-length seam.  The certificate's
-- relation to the paper's class is `EfficientlyComputable.toMachine`, audited above.
#assert_axioms_clean
  PolyFueled.primrec gcdc_polyFueled not_polyFueled_two_pow
  EF.cost_le_serialize_length EF.serialize_length_le_cost
  Strategy.serializeTrades_length_le_cost

-- dd:fuel digit layer (`def:ec`): the digit stream determines the token stream
-- (round-trip + injectivity), and every token-model certificate transfers into the
-- digit-metered class (the inclusion capstone).  The digit model is the
-- metering underneath the collapsed criterion class `EfficientlyComputable`.
#assert_axioms_clean
  undigitize_digitize digitize_injective
  PolySegStream.digitizeStream
  EfficientlyComputableTok.toDigit

-- dd:fuel discharged for dd:luv-arith: the threshold-code and process-computability
-- certificates are proved (gcdc_polyFueled/toLUV_polyThresholdCodes/gridDP_computable),
-- so these endpoints are FULLY unconditional over the constructed LIA — the sole
-- hypothesis is the rational bound/identity on the LUV values.
#assert_axioms_clean
  ComputableLUV.lic_expectation_provind_arith_unconditional
  ComputableLUV.lic_expectation_provind_le_arith_unconditional
  ComputableLUV.lic_expectation_provind_eq_arith_unconditional
  ComputableLUV.lic_linearity_of_expectation_arith_unconditional
  lic_no_expected_net_update lic_no_expected_net_update_conditional
  LUVCombination.BoundedSequence.recurringunbiasednessexp
  LUVCombination.BoundedSequence.prandexp
  LUVCombination.BoundedSequence.prandexp_below
  LUVCombination.BoundedSequence.prandexp_eq

-- Properties/MetaLearning.lean
#assert_axioms_clean
  lic_belief_finitistic_consistency
  lic_disbelief_inconsistent_theories lic_learns_halting_patterns
  lic_learns_provable_nonhalting_patterns lic_does_not_anticipate_halting

/-! ## Constructed boundary witnesses and their direct criterion consumers

Each block below names the file whose constructions *discharge* an interface the property
tail would otherwise assume, together with the criterion endpoints that consume them. -/

-- Construction/Witnesses/BoundedEvaluation.lean — the bounded-`evaln` compiler, repeated
-- enumeration of a c.e. set, settlement/patient clocks, and the prefix-freeze certificate.
#assert_axioms_clean
  codeEvalnNat_polyFueled
  EfficientRepeatedEnumeration.ofBig EfficientRepeatedEnumeration.ofCE
  lic_uniform_nonDogmatism_ofCE
  SettlementChecker.ofComputations PatientSettlementClock.ofComputations
  liaFreezeBefore_preserves_ecTok

-- Construction/Witnesses/QuotationAffine.lean — the code-indexed quotation layer
-- (`dd:quote-code`) and the diagonal price fixed point it makes constructible.
#assert_axioms_clean
  diagonalPriceDecisionPart_partrec diagonalPriceDecisionCode_eval
  diagonalPriceQuotePos_iff diagonalPriceQuoteNeg_iff diagonalPriceFixedpoint_spec
  parameterizedDiagonalQuoteCodeOfMarket
  parameterizedDiagonalQuoteCodeOfMarket_public_fixedpoint
  lic_introspection_ofCode lic_paradox_resistance_ofDiagonal
  lic_expectations_of_probabilities_ofCode lic_iterated_expectations_ofCode
  lic_self_trust_ofRepresentation lic_expected_future_expectations_ofRepresentation
  lic_no_expected_net_update_ofRepresentation
  lic_no_expected_net_update_conditional_ofRepresentation
  theoremMarketComputation paperMarketComputation paperQuotationPresentation
  paperDiagonalQuoteCode
  lic_paradox_resistance_ofDiagonal_unconditional

-- Construction/Witnesses/FeedbackEmission.lean — the emitter that turns a feedback
-- trader schedule into an `def:ec`-certified trade stream.
#assert_axioms_clean
  feedbackTraderEmissionSigns lic_wubaff_ofFeedbackTruth
  boundedCombination_wubaff_ofFeedbackTruth luv_wubexp_ofFeedbackTruth

-- Construction/Witnesses/FeedbackTruth.lean — the delayed-truth bridge: a computation of
-- the feedback value, clocked to the deferral day, feeding the unbiasedness endpoints.
-- `FeedbackTruth.ordinaryFeedbackTruthComputation` inhabits the delayed-truth premise with
-- a constant value stream (inhabitation only — see its docstring);
-- `FeedbackTruth.alternatingFeedbackTruthComputation_nonempty` is the **non-degenerate**
-- witness, whose stream takes both values along the deferral image, so the endpoints'
-- dependence on `truth` is exercised by an actual inhabitant and not only by the
-- arbitrary-`truth` statement.  `FeedbackTruth.exists_nonconstant_feedbackTruthComputation`
-- records that non-constancy explicitly; it carries no `Paper node:` line and so is
-- deliberately not asserted here.
#assert_axioms_clean
  FeedbackTruth.ordinaryFeedbackTruthComputation
  FeedbackTruth.alternatingFeedbackTruthComputation_nonempty
  feedbackTruthSequence feedbackTruthSequence_ofDetermined
  lic_wubaff_ofComputation lic_wub_ofComputation
  boundedCombination_wubaff_ofComputation luv_wubexp_ofComputation
  lic_wub_ofComputation_unconditional lic_wubaff_ofComputation_unconditional
  boundedCombination_wubaff_ofComputation_unconditional
  luv_wubexp_ofComputation_unconditional

-- Construction/Witnesses/BitPrefixSyntax.lean — the prefix-sentence family over
-- independent bit atoms, its token-metered naming emitter, and the semimeasure-domination
-- endpoint they feed.  `ordinaryBitPrefixSentences` is the **inhabitation witness** for
-- `BitPrefixSentences`; `not_polySentenceCodes_bitPrefixSentence` records why that field must
-- be metered in tokens rather than in the pair-code value.
--
-- Two witness layers, and which one to cite (final audit).  `ordinaryBitPrefixSentences`
-- lives over `emptyBitDeductiveProcess`, whose every stage is `∅`, so its `realizable` field
-- is discharged VACUOUSLY: it is an INHABITATION witness only, and the paper's
-- Θ-load-bearing reading of `thm:dus` is not exercised by it.  What it does exercise is the
-- naming half, which is the forced one: `ordinaryBitPrefixCodes` is a genuine write-out
-- emitter and the whole-value form of that field is unsatisfiable outright.
-- `paperIndependentBitAtoms` / `paperBitPrefixSentences` are the SUBSTANTIVE layer, over
-- `paperDP T`, whose stages are non-empty: independence is realized there by grafting a bit
-- assignment at the reserved atom tag 7, disjoint from the process's own atoms.  Cite the
-- paperDP layer, not the ordinary one, when asked whether the `thm:dus` premises are
-- non-vacuously satisfiable.  Both endpoints remain proved for an arbitrary deductive
-- process, so neither layer's limits bound the theorem.  See the declarations' docstrings.
#assert_axioms_clean
  not_polySentenceCodes_bitPrefixSentence ordinaryBitPrefixCodes
  bitPrefixSentencesOfIndependentAtoms ordinaryBitPrefixSentences
  lic_domination_universalSemimeasure_ofIndependentAtoms
  paperIndependentBitAtoms paperBitPrefixCodes paperBitPrefixSentences
  lic_domination_universalSemimeasure_paperDP

-- Construction/Witnesses/UniversalDovetailer.lean — the universal continuous semimeasure.
-- The universal continuous semimeasure is fully constructed: the semimeasure laws, the
-- monotone from-below stage table, the explicit domination constant, and the emission
-- program for the stage table (column tabulation).  The *polynomial* clock is now
-- discharged as well: the self-clamped stage table reads the fixed exact emitter under a
-- polynomial `evaln` clock, so both `DUSApproximationPresentation` and
-- `DUSThresholdEmission` are constructed objects.
#assert_axioms_clean
  Dovetail.continuousSemimeasure Dovetail.universalMass_dominates
  Dovetail.exists_universalApprox_code Dovetail.universalSemimeasure
  Dovetail.gridApprox_le_mass Dovetail.gridApprox_tendsto
  Dovetail.isPolyBounded_encode_gridApprox
  Dovetail.dusApprox_tendsto Dovetail.dusApprox_polyRatCodes
  Dovetail.dusApproximationPresentation Dovetail.dusThresholdEmission

-- Construction/Witnesses/StrictSeparators.lean — the recursively inseparable pair and the
-- null stage classes that make the strict-domination separator presentation constructible.
-- The separator presentation is fully constructed: Kleene's pair is recursively
-- inseparable, the constraint theory's enumerator is built from the atom codes, and the
-- stage classes are null (`separatorClass_mass_tendsto_zero`, the Kučera–Demuth argument)
-- rather than assumed.  `strictSeparatorPresentationOfKleene`'s only input is
-- computability of the atom Gödel codes, itself proved for the repo's atoms.
#assert_axioms_clean
  kleene_recursively_inseparable no_ce_null_prefix_family
  separatorClass_mass_tendsto_zero strictSeparatorPresentationOfKleene
  ordinaryAtom_code_computable
  lic_strict_domination_universalSemimeasure_ofAtomCodes

-- Construction/Witnesses/ConditioningPresentation.lean — the conditioning presentation
-- (condition sentences plus their codes) built from the process computations.
-- The compact interface's two witnesses: the degenerate one (empty adjoined process,
-- inhabitation only) and the growing one, which is what carries the content burden.
#assert_axioms_clean
  conditioningPresentationOfComputations fixedConditioningPresentation
  lic_conditioned_gated_ofComputations
  growingConditionProcessComputation growingCompactConditioningProcessComputation
  growingConditionProcess_ssubset
  deductiveStageCondition_growing_ne deductiveStageCondition_growing_ne_top
  prefixProcess prefixProcessComputation prefixConditioningPresentation

-- Construction/Witnesses/ConditioningCompiler.lean — the eventual price floor the
-- conditioning translation needs.  (The `def:ec`-preserving translations themselves are
-- the `_ecRpn` endpoints below, at the criterion's own class.)
#assert_axioms_clean
  exists_eventual_condition_price_floor
  eventualConditioningFloorOfJointConsistency

-- Construction/Witnesses/DigitConditioning.lean — the conditioning translation in the
-- digit metering model: guarded compilers, guard honesty, and the digit-to-digit
-- preservation results.
#assert_axioms_clean
  ConditioningCompile.strategyOfTokens_trades_eq_nil_of_bigDay
  ConditioningCompile.guardedConditionRun_polySegStream
  ConditioningCompile.guardedZeroAwareConditionRun_polySegStream
  ConditioningCompile.safeSeparatedFrameDigitOutput_polySegStream
  ConditioningCompile.conditionedTranslation_preserves_ecDigit
  ConditioningCompile.eventualConditionedTranslation_preserves_ecDigit

-- Construction/Witnesses/RpnConditioning.lean — the conditioning translation in the RPN
-- symbol model: the run-aware price transducer and its master commutation, guard honesty,
-- the frame pass and its gated two-leg join, and the two `def:ec → def:ec` translation
-- endpoints.  The `thm:scon` packaging that used to close this block now lives in
-- `Construction/Machine/CondEndpoints.lean`, listed below: criterion endpoints sit above
-- both the fuel and the machine realization rather than inside either.
#assert_axioms_clean
  RpnConditioning.rpnGuardedConditionRun_polySegStream
  RpnConditioning.rpnGuardedZeroAwareConditionRun_polySegStream
  RpnConditioning.unRpn_rpnConditionRun
  RpnConditioning.unRpn_rpnZeroAwareConditionRun
  RpnConditioning.strategyOfTokens_rpnGuardedConditionTokens_trades
  RpnConditioning.strategyOfTokens_rpnGuardedZeroAwareConditionTokens_trades
  RpnConditioning.rpnTradeCountAt_eq_frameTradeCount
  RpnConditioning.rpnStructurallyAccepts_agree
  RpnConditioning.rpnSafeSeparatedFrameOutput_polySegStream
  RpnConditioning.strategyOfTokens_unRpn_rpnSafeSeparatedFrameOutput_trades
  RpnConditioning.conditionedTranslation_preserves_ecRpn
  RpnConditioning.eventualConditionedTranslation_preserves_ecRpn
  RpnConditioning.strategyOfTokens_rpnConditionOutput
  RpnConditioning.strategyOfTokens_rpnZeroAwareOutput

-- Construction/Machine/CondStep.lean — the conditioning transduction in the machine model:
-- the same token-level automaton as the fuel realization, driven as a `Complexity.FP` client
-- of `TokenFold.runFold`, and the transport theorem the machine criterion needs.
-- Both transport theorems take the *same* `BigSentenceCodes` hypothesis on the condition
-- sequence as their fuel counterparts — `def:ec`'s own write-out class, in which a
-- condition's Gödel code may be exponential in the day — so nothing about `ψ` is weakened;
-- their trader hypothesis is the machine class, so they are strictly stronger there.
-- The bridge to the transducer's block discipline is `CondStep.machineSentenceBlocks_of_big`,
-- clocked by `BigTokenStream.digitizeStream`.
#assert_axioms_clean
  CondStep.conditionedTranslation_preserves_machine
  CondStep.eventualConditionedTranslation_preserves_machine

-- Construction/Machine/CondEndpoints.lean — the `thm:scon` packaging: operational witnesses
-- and criterion-level closure, over both realizations.  The block moved here unchanged from
-- `RpnConditioning.lean`; only the machine endpoint is new.
-- All three witnesses carry both certificates; the eventual one's machine field arrived
-- with its emitter (the finite-zero price rewrite, whose zero-day test is a fixed-finite-set
-- dispatch clamped at the floor's cutoff).  `thm:scon` stands at the paper's own quantifier
-- in all three forms.
#assert_axioms_clean
  ConditioningCompile.eventualConditioningOperationalWitness
  ConditioningCompile.gatedConditioningOperationalWitness
  ConditioningCompile.denominatorPatchedGatedConditioningOperationalWitness
  ConditioningCompile.lic_conditioned_gated_ofMarketComputation
  ConditioningCompile.lic_conditioned_gated_machine_ofMarketComputation
  ConditioningCompile.lic_conditioned_eventualOfFloor
  ConditioningCompile.lic_conditioned_eventualOfFloor_machine
  ConditioningCompile.lic_conditioned_eventual_ofMarketComputation
  ConditioningCompile.lic_conditioned_eventual_machine_ofMarketComputation
  ConditioningCompile.lic_conditioned_fixed_ofComputationAndMarket
  ConditioningCompile.lic_conditioned_growing_ofComputationsAndMarket
  ConditioningCompile.lic_conditioned_fixed_machine
  ConditioningCompile.lic_conditioned_growing_machine_ofProcessComputation
  ConditioningCompile.lic_conditioned_growing_machine_ofSequence
  ConditioningCompile.lic_conditioned_gated_ofComputationsAndMarket

-- Construction/Witnesses/RpnFreeze.lean — the prefix-freeze transducer in the RPN symbol
-- model, the run-level quote lookup, and the spelling characterization the lookup rests on.
--
-- MACHINE CLASS: closed.  `RpnFreeze.parseRpnLegacy_iff_patMatch` says a run denotes a
-- target exactly when it matches one of the target's finitely many spelling PATTERNS —
-- literal grammar tokens with a hole wherever an escape leaf may stand — so the lookup is a
-- fixed-depth automaton rather than a parser; `FreezeStep` runs the resulting transducer
-- through `TokenFold.runFold_mem_FP`; `FreezeOracle` supplies the lookup for any finite
-- table and compiles the patch from the market's own certificate.
-- The public statement is `FreezeOracle.machine_lic_iff_of_finiteSupport`: finite support
-- and computability of both markets, and NOTHING ELSE — no patch hypothesis, and no
-- condition of any kind on the finitely many sentences whose price moves.
--
-- FUEL CLASS: still open, and this is a true negative.  `EfficientPrefixPatch` and
-- `FiniteSupportPatch` remain uninhabited: the emitted segment's fuel certificate needs a
-- `BigDigits` decode test on exponentially large escape codes, and the digit model is not
-- closed under that inverse operation (`dd:fuel`).  `lic_iff_of_finitePerturbation` is
-- therefore still the only fuel-class coverage of `thm:ifp`.
--
-- THE `⊥` NARROWING IS GONE, and this is the substantive change.  It used to be the thing
-- that made the machine class work: `decode_eq_some_iff_of_botFree` proves Foundation's
-- decoder injective off the `⊥` fiber, so on a `⊥`-free target the escape-leaf test is a
-- comparison against a fixed numeral, while `decode_falsum_noncanonical` /
-- `decode_and_noncanonical` show the fiber really is infinite otherwise.  Those witnesses
-- now motivate the parser instead of restricting it: `DigitFP.sqrtRemW_mem_FP` and
-- `DigitFP.unpairW_spec` put base-4 integer square root and `Nat.unpair` in
-- `Complexity.FP`, `FiberTest.fiberW_mem_FP` builds the decode test on top of them (its
-- correctness is `sentenceMatches_eq_one_iff`, already proved both ways), and
-- `PatAuto.ifParse_mem_FP` is the recognizer that consumes it.  So `BotFree` is DISCHARGED,
-- not assumed.
--
-- `NoReserved` IS GONE TOO, and it stood for TWO devices, not one.  A structured
-- paper-prime leaf is spelled `[1, 0, pol] ++ 1^L ++ [0] ++ p ++ [19]` with `L = |p|`.
--   (i) The LENGTH IDENTIFICATION.  `L` is unbounded even for a fixed target because
--   `parseStructuredNat` has a self-loop at the numeral `0` (`1^k 0` spells `0` for every
--   `k`), so matching the unary field against the payload's own length is `a^n b^n`: no
--   finite-state device decides it, and no extension of a spelling list or of
--   `RunAuto.BlockAutomaton` could have.  `CtrAuto.ctrMachine` does — `BlockMachine`
--   instantiated as a finite control paired with one unary counter.
--   (ii) The PAYLOAD LANGUAGE: which token strings denote the fixed formula code.  This is
--   the larger half, it was NOT anticipated when `NoReserved` was first disclosed, and it
--   is not a spelling list either, since numeral padding and the double negation `[20, 20]`
--   both preserve a code.  `PayAuto` decides it exactly by top-down predictive parsing
--   against a stack of obligations that carries the pending negation as a PARITY BIT rather
--   than applying `negFormulaCode`; that keeps every child code an `unpair` component of its
--   parent, so a potential argument bounds the reachable stacks and the state set is finite.
--   Soundness of the parity step needs `negFormulaCode` to be an involution ON THE PARSER'S
--   RANGE — it is NOT one on `Nat`, where tags 2/3 discard their payload
--   (`PayAuto.WFCode`).
-- `StructPat.parseRpn_iff_segMatch` is the unconditional characterization the two hang on,
-- and `SegRec.ifParseFull_mem_FP` the resulting polynomial-time decision.
--
-- WHAT IS DISCLOSED IN THEIR PLACE is a property of the CONSTRUCTION, not of the statement:
-- the recognizer is compiled per frozen sentence, so its polynomial-time witness carries
-- constants (the automaton's state bound) depending on that sentence.  That is exactly the
-- paper's own "finitely many constants can be hard-coded", and it is sound precisely because
-- the support is finite — the point at which the printed finite-DAYS proof breaks and this
-- one does not.
--
-- CAREFUL, two different "unrestricted" statements meet here.  The finite-SUPPORT statement
-- without any syntactic condition — same two computable markets, differing on finitely many
-- `(day, sentence)` coordinates — is now PROVED
-- (`FreezeOracle.machine_lic_iff_of_finiteSupport`).  The PAPER's unrestricted statement,
-- tail agreement past some day `N`, is a different and STRONGER claim, and it is FALSE:
-- `FinitePerturbationCounterexample.not_overgeneral_ifp` refutes it (PE1).  Do not read the
-- first as retracting the second.  The two hypotheses are separated mechanically:
-- `FiniteSupportPerturbation.tail_agree` gives finite coordinate support => eventual day
-- agreement, and `tailAgree_not_finiteSupport` shows the converse fails, so the corrected
-- theorem cannot re-derive the refuted one.
#assert_axioms_clean
  EF.strategyOfTokens_freezeTokenRunOn_trades
  MachineEfficientTrader.freezeOn
  RpnFreeze.matchRun_iff
  RpnFreeze.runPrefixQuoteFromStates_exact
  RpnFreeze.unRpn_rpnFreezeRun
  RpnFreeze.unRpn_rpnFreezeRunOn
  RpnFreeze.freezeStreamRewriter_of_flatPass
  RpnFreeze.parseStructuredPaperPrime_shape
  RpnFreeze.spellings_sound
  RpnFreeze.spellings_complete
  RpnFreeze.parseRpnLegacy_iff_mem_spellings
  RpnFreeze.parseRpn_imp_parseRpnLegacy
  RpnFreeze.parseRpn_iff_mem_spellings
  RpnFreeze.patterns_sound
  RpnFreeze.patterns_complete
  RpnFreeze.parseRpnLegacy_iff_patMatch
  RpnFreeze.parseRpn_iff_patMatch
  RpnFreeze.matchRun_eq_matchRunCanon
  decode_eq_some_iff_of_botFree
  sentenceMatches_of_botFree
  decode_falsum_noncanonical
  decode_and_noncanonical

-- Construction/Witnesses/FreezeStep.lean — the freeze transducer as a `Complexity.FP`
-- client of `TokenFold.runFold`, over the FLAT stream (the one a machine holds), reusing
-- `CondStep.condStepR` as its automaton.  `decodeBits_freezePass` says the pass computes
-- `rpnConditionRun (RpnFreeze.freezeEmitOn selRun quoteRun)` exactly — no day clamp, since
-- the freeze oracle's output is bounded by a constant where the conditioning oracle's is
-- not.  `freezeStreamRewriter_of_runOracle` closes the chain to `FreezeStreamRewriter`.
-- ALL of it is conditioned on a `FreezeStep.RunOracle`.  That structure is now INHABITED
-- (`FreezeOracle.runOracleOf`), so the chain closes; see the FreezeOracle block below for
-- what the inhabitant assumes and what it still does not supply.
-- The lookup's shape is settled too: `RpnFreeze.spellings` is the FINITE list of complete
-- legacy spellings of a target, and `spellings_sound` proves each member parses.  Under the
-- two side conditions (`BotFree`, and the target outside the reserved `atom (pair 7 _)`
-- shape) deciding "does this run denote ψ" is membership in that list, so NO streaming
-- automaton has to be proved to agree with `parseRpn`.  Both directions are now proved
-- (`parseRpnLegacy_iff_mem_spellings`), with `BotFree` load-bearing for exhaustiveness.
-- The full-grammar form `parseRpn_iff_mem_spellings` is now proved too, bridged by
-- `parseRpn_imp_parseRpnLegacy` (costing the `NoReserved` side condition) and the upstream
-- `parseRpn_of_legacy`.  All of this is RECOGNITION only: turning "membership in a list of
-- constants" into a `Complexity.FP` test, and thence into a `FreezeStep.RunOracle`, is not
-- done.  No `RunOracle` instance exists, so no patch structure is inhabited.
-- The table side conditions are collected in `CanonicalCodes.lean`'s "The recognition side
-- conditions, in one place": `Recognizable` (= `BotFree` + `NoReserved`) per sentence, plus
-- the constant output bound on the table as a whole.  Only the last is still assumed; both
-- halves of `Recognizable` are discharged by the recognizer chain
-- (`StructPat` / `PayAuto` / `CtrAuto` / `SegAuto` / `SegCtr` / `SegRec`).
#assert_axioms_clean
  FreezeStep.decodeBits_flatEmitR
  FreezeStep.freezePass_mem_FP
  FreezeStep.decodeBits_freezePass
  FreezeStep.freezeStreamRewriter_of_runOracle

-- Construction/Witnesses/FreezeOracle.lean — the run-level lookup, and with it a
-- `FreezeStep.RunOracle` for any finite table (`runOracleOf`).  This CLOSES the freeze
-- chain: `machineFiniteSupportPatch_ofTable` inhabits `MachineFiniteSupportPatch` for any
-- market whose frozen table is presented by a recognizable entry list, and
-- `machineFiniteSupportPatch_example` / `_pair` do so at a table with a REAL row
-- (`exampleS_nonempty`), so the degenerate empty-table discharge is not what is happening.
-- SIDE CONDITIONS: THERE ARE NONE LEFT on the sentences.  `TablePresentation` is not one:
-- `entriesOf` reads the entry list off `S` and the market's own quote table, so
-- `machineFiniteSupportPatch` needs only `ComputableMarket`, and the public
-- `machine_lic_iff_of_finiteSupport` carries no patch hypothesis and no syntactic condition
-- at all.  `machine_lic_iff_of_noReservedSupport` and `machine_lic_iff_of_recognizableSupport`
-- are retained as one-line compatibility corollaries, not as the strongest statement.
-- The constant output budget is DERIVED here (`oracleOf_length_le`), not assumed.
-- What IS disclosed is a property of the construction rather than the statement: the
-- recognizer is compiled per frozen sentence, so its polynomial-time constants depend on
-- that sentence — the paper's own hard-coded finite table, sound because the support is
-- finite.
-- STRICTNESS is proved, not asserted, and now at BOTH retired conditions, at the
-- PERTURBATION level (not merely the sentence level): `not_recognizableSupport_hardPoint`
-- proves `¬ RecognizableSupportPerturbation` of the `hardSentence` market pair outright, and
-- `not_noReservedSupport_reservedPoint` proves `¬ NoReservedSupportPerturbation` of the
-- `reservedSentence` pair — each ruling out *every* admissible support set by forcing the
-- differing coordinate into it (`pointHistory_ne_at`), which a sentence-level negative alone
-- cannot do.  `machine_lic_iff_hardPoint` then applies the new endpoint at
-- `hardSentence = atom 0 ⋏ ⊥` (which fails `BotFree`) and `machine_lic_iff_reservedPoint` at
-- `reservedSentence` (a reserved atom failing `NoReserved`), each over a concrete pair of
-- `ComputableMarket`s that genuinely differ there (`computableMarket_point`,
-- `pointHistory_ne_at`).  (`not_recognizable_hardS` / `not_noReserved_pointS_reserved` remain
-- as the underlying sentence/set-level facts, but are not themselves the unreachability
-- witnesses.)
-- The market pair is now supplied too: `computableMarket_twoPoint` builds two honest
-- `ComputableMarket`s (rational table plus a `Nat.Partrec.Code` on the PAIRED input, so day
-- zero gets no free special-casing), `twoPointHistory_ne_at` exhibits their disagreement,
-- and `machine_lic_iff_twoPoint` is the corrected `thm:ifp` at that pair with NO remaining
-- hypotheses.  So the theorem's antecedent is satisfiable: it is non-vacuous.
-- That pair is non-vacuous but not informative on its own: those markets price almost
-- everything at zero and are very likely exploitable, so the equivalence may hold there
-- because both sides are false.  The informative instance is in
-- Construction/Witnesses/LIAPerturbation.lean; see that block.
#assert_axioms_clean
  FreezeOracle.decodeBits_oracleOf
  FreezeOracle.oracleOf_mem_FP
  FreezeOracle.runOracleOf
  FreezeOracle.machineFiniteSupportPatch_ofTable
  FreezeOracle.machineFiniteSupportPatch_example
  FreezeOracle.machineFiniteSupportPatch_pair
  FreezeOracle.exampleS_nonempty
  FreezeOracle.machine_lic_iff_example
  FreezeOracle.computableMarket_twoPoint
  FreezeOracle.twoPointHistory_ne_at
  FreezeOracle.machine_lic_iff_twoPoint
  FreezeOracle.machineFiniteSupportPatch_ofRecognizable
  FreezeOracle.machine_lic_iff_of_recognizableSupport
  FreezeOracle.machineFiniteSupportPatch_ofNoReserved
  FreezeOracle.machine_lic_iff_of_noReservedSupport
  FreezeOracle.machineFiniteSupportPatch
  FreezeOracle.machine_lic_iff_reservedPoint
  FreezeOracle.not_noReserved_pointS_reserved
  StructPat.parseRpn_iff_segMatch
  StructPat.segPatterns_sound
  StructPat.segPatterns_complete
  PayAuto.payAccepts_iff
  PayAuto.payAuto_iff
  PayAuto.nineteen_not_mem_of_parse
  CtrAuto.ctrMachine_accepts
  CtrAuto.ifCtr_mem_FP
  SegAuto.segAuto_accepts
  SegCtr.segMatch_iff_relaxed_and_ctr
  SegRec.segMatch_iff_accepts
  SegRec.ifParseFull_mem_FP
  FreezeOracle.not_botFree_hardSentence
  FreezeOracle.not_noReserved_reservedSentence
  FreezeOracle.not_recognizable_hardS
  FreezeOracle.not_recognizableSupport_hardPoint
  FreezeOracle.not_noReservedSupport_reservedPoint
  FreezeOracle.computableMarket_point
  FreezeOracle.pointHistory_ne_at
  FreezeOracle.machine_lic_iff_hardPoint
  FiniteSupportPerturbation.tail_agree
  DigitFP.sqrtRemW_mem_FP
  DigitFP.unpairW_spec
  FiberTest.fiberW_mem_FP
  FiberTest.holeGuards
  PatAuto.ifParseLegacy_mem_FP
  PatAuto.ifParse_mem_FP
  RunAuto.guardedAutomaton
  RunAuto.BlockAutomaton.ifAuto_mem_FP
  tailAgree_not_finiteSupport

-- LogicalInduction/API.lean — the consumer-surface name for the corrected `thm:ifp`.
-- `lic_iff_of_recognizableSupportPerturbation` is a thin public wrapper, definitionally the
-- `FreezeOracle` theorem asserted just above; it exists so a client cites a root-namespace
-- name rather than a construction namespace.  Asserted here because it carries a
-- `Paper node:` line, and the per-declaration gate admits no annotated declaration that no
-- `#assert_axioms_clean` block names.  It is NOT public canonical trust surface: the
-- LI-CANONICAL block is exactly the endpoints table of `scripts/coverage-classification.md`,
-- and `thm:ifp`'s canonical endpoint there is unchanged.
#assert_axioms_clean
  lic_iff_of_finiteSupportPerturbation_machine
  lic_iff_of_noReservedSupportPerturbation
  lic_iff_of_recognizableSupportPerturbation

-- Construction/Witnesses/LIAPerturbation.lean — the corrected `thm:ifp` doing visible work.
-- `liaHistory DP` is a machine logical inductor; `liaPerturbed` moves ONE price, at the
-- `Recognizable` coordinate `(0, atom 0)`, and `machineLogicalInductor_liaPerturbed` derives
-- that the result is still one.  Nothing else in the repo derives that: the perturbed market
-- is not the output of any construction, so its inductor-hood is exactly what the theorem
-- buys.  `computableMarket_liaPerturbed` rebuilds the market program (the code is combined at
-- the `Nat.Partrec` level, since `ComputableMarket` hands over a code rather than a
-- `Computable` function), and `liaPerturbed_ne` proves the price change NONZERO, so this is
-- not the degenerate `P = P'` route by a third door.
-- It remains conditional on the same two hypotheses `Construction/LIA.lean` carries: the LIA
-- market program and a computable deductive process.  Nothing here discharges those.
#assert_axioms_clean
  LIAPerturbation.computableMarket_liaPerturbed
  LIAPerturbation.machineLogicalInductor_liaPerturbed
  LIAPerturbation.exists_informative_liaPerturbation

-- Construction/Witnesses/UnconditionalOverLIA.lean
#assert_axioms_clean
  lic_domination_universalSemimeasure_unconditional
  lic_domination_dovetailSemimeasure_unconditional
  lic_domination_everyLowerSemicomputable_unconditional
  lic_domination_dovetailSemimeasure_paperDP
  lic_domination_everyLowerSemicomputable_paperDP
  lic_strict_domination_universalSemimeasure_unconditional
  lic_conditioned_ofCompiler_unconditional
  lic_conditioned_fixed_unconditional
  lic_conditioned_growing_unconditional
  lic_conditioned_fixed_machine_unconditional
  lic_conditioned_growing_machine_unconditional
  exists_growing_conditioned_machine_inductor

-- Construction/Witnesses/LUVSyntax.lean — LUV-combination syntax, the mesh-softmax
-- operational witness it constructs (`lem:mesh`), and the four expectation endpoints
-- that consume that witness with the operational hypothesis discharged
-- (`lem:mesh`, `thm:exppolymax`, `thm:expcoh`, `thm:perexpkno`).
-- `ordinaryLUVCombinationSyntax` (QuoteCodeOfMarket.lean) is the constructed
-- non-vacuity witness for the `_ofSyntax` endpoints' caller data, over a
-- non-degenerate index-varying sequence.
#assert_axioms_clean LUVCombinationSyntax.meshSoftmaxOperationalWitness
  ordinaryLUVCombinationSyntax

-- Construction/Witnesses/PaperLUV.lean, StructuredPaperRpn.lean, ArithmeticSource.lean —
-- the literal first-order frontend.  `PaperLUV` renders `def:luv` as an actual
-- `ArithmeticSemisentence 1` with object-level `T`-proofs of unique existence and
-- unit-interval membership; `toLUV` compiles it into the abstract threshold carrier and
-- `source_valued` *derives* the world value.  `PaperLUVCombination` states `def:blcp`
-- over that frontend rather than over the abstract carrier, and `boundedSequence`
-- discharges the bounded-combination-sequence interface the expectation theorems consume.
-- Both are inhabited by genuinely varying families, not constant stand-ins:
-- `invPaperLUV` builds the literal paper LUV of value `1/v` from any closed `ℒₒᵣ` term of
-- value `v`, and its two instances are `unitFracPaperLUVSeq` at `1/(n+1)` (denominator a
-- unary numeral) and `dyadicPaperLUVSeq` at `2⁻ⁿ` (denominator the compact numeral of
-- `2 ^ n`, `O(n)` symbols).  The second is what shows the token-metered class reaches the
-- superpolynomially small values the paper writes.
-- `PaperLUV.rpnThresholdCodes` is the single-LUV route out of the frontend: the constant
-- family reindexed along `m ↦ ⟨0, m⟩`, giving the non-sequence `LUV.RpnThresholdCodes` that
-- the whole-LUV endpoints take as a hypothesis (`LUV.expect_converges`, `thm:ec`), with no
-- efficiency side condition, since a constant formula family is trivially token-metered.
-- The metering is on the paper's **source**.  `PaperLUVSeq` carries each LUV's defining
-- formula as the paper writes it (`source : ℕ → ArithSource 1`, over the primitive
-- connectives `¬ ∧ ∨ ⟹ ⟺` of tex:560 and quantifiers `∀ ∃` of tex:571-577), a proof that it denotes the LUV's Foundation
-- formula (`compiles`), and `def:ec`'s condition on that writing (`structural`, i.e.
-- `PolyArithmeticSourceSeq`).  Normal-form expansion happens inside
-- `parseStructuredArithmeticFormula` (tags `20`/`21`/`22`), never on the emitted stream.
-- Two boundaries are recorded as named refutations, and they are of different kinds.
-- `unaryRendering_two_pow_not_polyArithmeticFormulaSeq` (with its source-class twin
-- `unaryRendering_two_pow_not_polyArithmeticSourceSeq`) is an artifact of Foundation's
-- *unary* `Semiterm.Operator.numeral`, not a narrowing of `def:ec`: the paper fixes no
-- numeral notation (underline convention, tex:564) and the value is nameable compactly inside `ℒₒᵣ`.
-- The compact numeral machinery it rests on (`binNumeral`, `binNumeralEnc_length_le`,
-- `binNumeral_val`, `binNumeralEnc_two_pow_polySegStream`) and the shared template
-- `invFormula` are internal — though `binNumeral` is no longer only a foil-avoidance
-- device: since the R5-F08 repair it is how the represented claim families below spell the
-- argument that names the machine (`polySegStream_binNumeralEnc`).
-- `iffChain_not_polyArithmeticFormulaSeq` is no longer a disclosure: it is the **strictness
-- separation** between the normal-form-metered foil `PolyArithmeticFormulaSeq` and the
-- paper's class `PolyArithmeticSourceSeq`.  Foundation's `Semiformula` has no `⟺`
-- constructor, so `A 🡘 B` duplicates both sides (`encodeArithmeticFormulaSymbols_iff`) and
-- the paper-linear left-nested chain `iffChain` costs `≥ 2ⁿ` tokens in the foil
-- (`two_pow_le_encode_iffChain`, both internal) — while the *same* family is certified in
-- the paper's class at `5n + 4` emitted tokens
-- (`iffChainSource_polyArithmeticSourceSeq`, `sourceTokens_iffChainSource_length`).
-- `iffPaperLUVSeq` is that family carried all the way to `LUV.RpnThresholdCodeSeq`
-- (`iffPaperLUVSeq_frontend`): a literal paper LUV family whose `n`-th defining formula is
-- `O(n)` characters to write and whose Foundation normal form has `≥ 2ⁿ` nodes.  With
-- `PolyArithmeticFormulaSeq.toSource` for the inclusion, `PolyArithmeticFormulaSeq ⊊
-- PolyArithmeticSourceSeq` is proved, not asserted.
#assert_axioms_clean
  PaperLUV.toLUV PaperLUV.source_valued
  PaperLUVSeq.rpnThresholdCodeSeq PaperLUVSeq.source_valued_and_rpnThresholdCodeSeq
  PaperLUV.rpnThresholdCodes
  invPaperLUV
  unitFracPaperLUVSeq unitFracPaperLUVSeq_frontend
  dyadicPaperLUVSeq dyadicPaperLUVSeq_frontend
  iffPaperLUVSeq iffPaperLUVSeq_frontend
  unaryRendering_two_pow_not_polyArithmeticFormulaSeq
  unaryRendering_two_pow_not_polyArithmeticSourceSeq
  iffChain_not_polyArithmeticFormulaSeq
  PaperLUVCombination.boundedSequence
  unitFracPaperLUVCombination unitFracPaperLUVBoundedSequence
#assert_axioms_clean
  LUVCombination.BoundedSequence.mesh_independence_ofSyntax
  LUVCombination.BoundedSequence.exppolymax_ofSyntax
  LUVCombination.BoundedSequence.expcoh_ofSyntax
  LUVCombination.BoundedSequence.perexpkno_ofSyntax

-- Construction/Witnesses/ComputationSyntax.lean — the claim-name syntax shared by the
-- meta-learning lanes.  Every *endpoint* has left this file.  The *bounded* lane that used
-- to live here — the `BoundedComputation` carrier, its two non-vacuity witnesses, the
-- represented decidable claims over it and the two finite-consistency `_ofComputation`
-- endpoints — is **retired**: `thm:pac` and `thm:pazfc` are stated directly at the
-- arithmetized `Con(Θ′)` family (`ComputationRepresented.lean`), which leaves no caller for
-- a caller-supplied bounded computation.  `thm:dontwait`'s bounded family is
-- `representedBoundedHaltingClaims`, audited under that heading below.  The **unbounded
-- halting lane** has moved the same way and for the same reason:
-- `representedHaltingClaims`, `lic_learns_halting_patterns_ofComputation` and
-- `lic_learns_provable_nonhalting_patterns_ofComputation` are stated over `paperTheoryDP`
-- at the day-indexed halting schema, and are listed under that heading below rather than
-- here.  The **`thm:incons` lane** has now moved too (tranche 8): it is stated over
-- `paperTheoryDP` at the base theory's provability schema, so `SemidecidableComputation`,
-- its `ordinarySemidecidableComputation` `0 < n` witness (superseded by a witness whose
-- day-`n` theory is an actually inconsistent theory),
-- `inconsistentTheoryClaimsOfComputation` and
-- `lic_disbelief_inconsistent_theories_ofComputation` are all **retired**.  What remains in
-- this file is the claim-name syntax (`computationClaimSentence` and its digit lemmas) and
-- the presentation interface.

-- Framework/RepresentsComputations.lean — the paper's representability premise.
-- `RepresentsComputations T` is the Lean rendering of the paper's standing §2 assumption
-- that `Θ` *represents computations* (tex:600-606): for every total computable `f` there
-- is a two-variable formula `γ_f` with `y = f n ↔ T ⊢ ∀ν (γ_f(n̄, ν) ⟺ ν = ȳ)`.  It is a
-- condition on what `T` *derives*, with no reference to truth in the standard model, and
-- it is the interface that replaces Σ₁-soundness wherever the paper's own argument needs
-- only the paper's own premise.  `represents_refutes` / `represents_refutes_all` are the
-- negative literals that weak Σ₁-representation cannot supply; they consume `[𝗥₀ ⪯ T]`
-- only, and no semantic hypothesis.  `reprAllSchema_subst` is what keeps the claim family
-- enumerable by the *fixed*-schema machinery even though `γ` is supplied existentially.
-- NOT YET INVENTORIED.  `scripts/check-paper-nodes.sh` requires every name in an
-- `#assert_axioms_clean` block to carry a `Paper node:` docstring line, and none of this
-- file's declarations does yet — the class and its two literals
-- (`RepresentsComputations`, `represents_proves`, `represents_refutes`,
-- `represents_refutes_all`, `reprAllSchema_subst`, `RepresentsComputations.consistent`,
-- `numeral_ne_prov`, `numeral_eq_refl_prov`, `subst_subst_two`, `subst_iff_numeral`) are
-- all axiom-clean (`[propext, Classical.choice, Quot.sound]`; `numeral_ne_prov` is
-- `[propext, Quot.sound]`) but are inventoried only transitively, through the endpoints
-- below that consume them.  Annotating them (`thm:pac` / `thm:pazfc` / `thm:dontwait`, as
-- `ComputationTheoryPresentation` is annotated) is what unblocks a block here, and the
-- same applies to a `#assert_fields RepresentsComputations` freeze of its single field
-- `repr`.

-- Framework/DerivationSize.lean — the §4.10 symbol measure.  Foundation exposes no size
-- function on its internal derivations, so this module builds one: `dSize : ℕ → ℕ`, the
-- symbol count of a derivation code, by external recursion at `V := ℕ`.  Two things make it
-- usable.  (i) Faithfulness: `dSize_axL`, `dSize_cutRule`, … tie it to Foundation's own
-- derivation constructors, and `mem_iff_testBit` identifies the sequent bitset's members
-- with the bits `sSize` sums over.  (ii) The converse bound `le_G_dSize : d ≤ G (dSize d)`
-- for a computable monotone tower `G` — `dSize d ≤ d` is the useless direction; this is the
-- one that turns "some derivation of at most `k` symbols" into a *finite* search and so
-- keeps the metered predicate decidable in both polarities.  The counting convention (one
-- symbol per rule name / connective / quantifier / predicate / function symbol / variable
-- occurrence, one separator per argument-list entry, and, per index, its binary digit count
-- plus one marker token — `idxLen n = Nat.size n + 1`, the marker being what separates an
-- index numeral from the following material) is `dd:symbolcount`, stated in that module's
-- header; the paper fixes neither an encoding nor an alphabet, so a convention is
-- unavoidable and no substitution is charged.
-- NOT YET INVENTORIED — none of this module's declarations carries a `Paper node:` line
-- (the measure is a convention supporting `thm:pac` / `thm:pazfc`, not a paper node of its
-- own), and `scripts/check-paper-nodes.sh` forbids unannotated names in an
-- `#assert_axioms_clean` block.  Axiom accounting for the module is therefore the
-- `#print axioms` footer at the foot of the file, which covers its whole public surface;
-- that footer is logging-only — the check is the human read of the build log, per the
-- audit doctrine, not a failing gate.

-- Framework/DerivationSizeComputable.lean — the computability layer for the §4.10 symbol
-- measure.  `DerivationSize.lean` defines `tSize`, `tvSize`, `fSize`, `sSize`, `dSize` and
-- the tower `G` by well-founded recursion at `ℕ`, which says nothing about effectivity;
-- this module proves each of them primitive recursive (hence computable) by Mathlib's
-- course-of-values recursor `Primrec.nat_strong_rec`, and adds
-- `computable_boundedSearchValue`, the bounded-existential search that
-- `BoundedConsistency.lean` spends to make `bProv` decidable in both polarities.  Nothing
-- here is a modeling choice: it is the effectivity half of `dd:symbolcount`, without which
-- the §4.10 proof search would be a classical existence statement rather than an algorithm.
-- NOT YET INVENTORIED — same reason as its base module: no declaration carries a
-- `Paper node:` line.  Axiom accounting is the `#print axioms` footer at the foot of the
-- file, covering all of its public lemmas; logging-only, checked by the human read of the
-- build log per the audit doctrine.

-- Framework/BoundedConsistency.lean — the §4.10 bounded-provability substrate.
-- `BProv T φ k` is "some `T`-derivation of the sentence coded by `φ` has `k` or fewer
-- symbols", over Foundation's internal `Bootstrapping.Proof` and `dSize`, with the bound
-- **inclusive** as the paper's is; `conWithin T k` is the paper's `Con(T)(k)` at that
-- measure.  (The former `dd:proofcode` substitution — metering by the derivation's Gödel
-- number — was retired in tranche 9a and is gone from the surface.)  Decidability is
-- obtained without a proof checker: `Proof` is `𝚫₁`, so the packed proof predicate and its
-- negation are both `𝚺₁` by `definability`, and `re_iff_sigma1` +
-- `ComputablePred.computable_iff_re_compl_re'` decide it; the *search* is then finite by
-- `bProv_iff_bounded`, which is where `le_G_dSize` is spent, giving
-- `bprovValue T : ℕ → ℕ`.  `conRunValue T' f` is the universal decider actually represented
-- by `thm:pac` and `thm:pazfc`; `conWithin_of_consistent` is the truth premise, derived from
-- consistency alone through `Bootstrapping.provable_of_standard_proof`.  The whole substrate
-- takes the metered theory `T'` as an ordinary parameter, independent of the representing
-- theory `T`: `thm:pac` is the diagonal `T' = T` (consistency from `RepresentsComputations`),
-- `thm:pazfc` a stronger `T'` (consistency an explicit hypothesis, the paper's own premise).
-- NOT YET INVENTORIED, for the same reason as `Framework/RepresentsComputations.lean`
-- above: `scripts/check-paper-nodes.sh` requires every name in an `#assert_axioms_clean`
-- block to carry a `Paper node:` docstring line, and these are internal `lemma`s and
-- `def`s that deliberately carry none — the paper node lives on the endpoint that consumes
-- them.  All are axiom-clean (`[propext, Classical.choice, Quot.sound]`, checked by the
-- `#print axioms` lines at the foot of that file) and are inventoried transitively through
-- `lic_belief_finitistic_consistency_unconditional`.

-- Construction/Witnesses/R0Representability.lean — the concrete instantiation, i.e. the
-- non-vacuity of `RepresentsComputations`: it holds for every theory extending `𝗣𝗔⁻` that
-- is true in `ℕ`, with instances registered at `𝗣𝗔⁻`, `𝗜𝚺₁` and `𝗣𝗔`.  Note the
-- asymmetry: standard-model truth is used to **verify** the premise for these particular
-- theories (Gödel completeness plus soundness) and by no *consumer* of the class, which is
-- why no endpoint inherits a semantic hypothesis from it.  It does **not** hold by this
-- argument at `𝗥₀`: Foundation's
-- `code_uniq` is stated for `𝗥₀` in a commented-out block, but `𝗥₀` has no trichotomy
-- axiom, so the `rfind` case of single-valuedness is unavailable there.  `𝗣𝗔⁻` is the
-- weakest theory in Foundation's hierarchy for which the argument closes.  Not inventoried
-- for the same reason as the block above: `representsComputations_of_peanoMinus` and the
-- three registered instances carry no `Paper node:` line yet.

-- Construction/Witnesses/SubstEmission.lean — numeral-substitution emission, and the
-- `def:ec` certificate for the represented claim family on the paper's SOURCE language.
-- `⟺` is a primitive of the paper's syntax (tex:560) and only a duplicating macro in
-- Foundation's negation normal form, so the body `γ(n̄,ν) ⟺ ν = 0̄` is metered as ONE `iff`
-- node over two leaves.  Nothing is assumed about `γ`: it may be `Classical.choice`-obtained.
-- This discharges what was previously the `hpoly` hypothesis of `representedBoundedClaims`.
-- Since the R5-F08 repair the *live* certificate path is the argument-term family — the
-- claim's argument is a closed term (a compact `binNumeral`), not a unary numeral — so what
-- the endpoints consume is `polyArithmeticFormulaSeq_subst_arg`, `schemaArgBody`,
-- `reprArgBodySource`, `reprArgClaimSource`, `schemaArgSource`, their `compile_*` and
-- `*_polyArithmeticSourceSeq` companions, and `bigSentenceCodes_reprArgClaim` /
-- `bigSentenceCodes_schemaArgClaim`.  The numeral-substitution family
-- (`polyArithmeticFormulaSeq_subst_numeral`, `compile_reprBodySource`,
-- `compile_reprClaimSource`, `reprBodySource_polyArithmeticSourceSeq`,
-- `reprClaimSource_polyArithmeticSourceSeq`, `rpnSentenceCodes_reprClaim`,
-- `bigSentenceCodes_reprClaim`) and the day-numeral schema family (`schemaDayBody`,
-- `schemaDaySource` and their companions) are retained — `schemaDayBody_eq_arg` records
-- that the day form is the argument form at the day numeral — but are no longer consumed by
-- any claim family.
-- Not inventoried yet, for the annotation reason recorded above: none of them carries a
-- `Paper node:` line.  They are covered transitively by the `ComputationRepresented.lean`
-- endpoints below.

-- Construction/Witnesses/ComputationRepresented.lean — the bounded *and* unbounded lanes
-- at the premise, with the machine named in the sentence.
--
-- **The design (R5-F08/F09 repair, 2026-08-30).**  What is *represented* here is a
-- UNIVERSAL object, fixed once per theorem and mentioning no machine sequence: the total
-- computable `universalRunValue steps` on the bounded lane — it decodes a packed
-- `⟨⟨source, input⟩, day⟩` argument, so `RepresentsComputations` supplies ONE `γ` per
-- horizon program, which is the paper's `⌜f⌝` (tex:600-606) — and the fixed r.e.
-- `universalHaltingSchema = codeOfREPred UniversalCodeHalts` on the unbounded lane.  The
-- machine and its input enter the *sentence*, as the argument written into that fixed
-- object and spelled by the compact Horner term `binNumeral` (`O(log v)` `ℒₒᵣ` nodes):
-- `binNumeral (haltingClaimInput (machines n) (inputs n))` on the unbounded lane and
-- `binNumeral (boundedArg machines inputs n)` on the bounded one.  That is what makes the
-- claim family depend on the machine sequence at all, and it is what
-- `hm : DigitMachineCodes machines` and `hi : BigDigits inputs` are consumed by — the
-- argument's symbol run is emitted digit by digit from those write-out certificates
-- (`boundedArg_digits`, `polySegStream_binNumeral_const`), so the two hypotheses are
-- load-bearing on the `def:ec` obligation rather than decorative.  Provability is
-- insensitive to the numeral spelling (`provable_subst_iff_of_val`, Gödel completeness in
-- both directions, needing only `𝗣𝗔⁻ ⪯ T`, which those endpoints now carry as their own
-- binder), so only the emission cost changes.
--
-- This replaces a rendering (through 2026-08-30) that built the family from
-- `codeOfREPred (fun n => CodeHalts (machines n) (inputs n))`, or from
-- `RepresentsComputations.repr` of a decider that mentioned the sequence.  Both see their
-- data only up to EXTENSIONAL equality, and each endpoint's own hypothesis pinned that
-- extension to a constant, so the family was literally one sentence family for every
-- admissible machine sequence.  The standing test against that failure mode is now proved
-- in-file rather than assumed, and since tranche 7 in its FULL syntactic form:
-- `haltingArgClaimSentence_ne_of_source_ne` separates two claim families by their machines'
-- source numbers ALONE, whatever those machines do, via the substitution-occurrence
-- machinery of `LogicalInduction/Framework/SubstOccurrence.lean` (`Semiformula.Mentions`,
-- `eq_of_rew_eq_of_mentions`) and the side condition
-- `universalHaltingSchema_mentions_zero`; `representedClaimSentence_ne_of_const_ne` is the
-- bounded-lane analogue, with the occurrence side condition on the existentially supplied
-- `γ` stated as a hypothesis.  The older behavioural pair
-- `haltingArgClaimSentence_ne_of_halts_ne` (unbounded) and
-- `representedClaimSentence_ne_of_runValue_ne` (bounded) show that data differing in
-- halting behaviour receive DIFFERENT claim sentences.  Neither carries a `Paper node:`
-- line — they are anti-vacuity witnesses, not paper claims — so neither is inventoried as
-- an endpoint; they are named here because they are the test any future represented claim
-- family has to pass.
-- The bounded-halting claim family is stated as the paper states it (`⌜f⌝(⌜n⌝)`), carried
-- by `paperTheoryDP` (which enumerates every `T`-provable proposition and therefore needs
-- no fixed schema).  Both public literals come from the *same* sentence: the positive one
-- and its literal negation, supplied by the representability premise.  The `thm:pac`,
-- `thm:pazfc` and `thm:dontwait` claim families live here, and no semantic hypothesis on
-- `T` remains at any of the three `_unconditional` endpoints — `hworld` is
-- `paperTheoryDP_nonvacuous`, which runs on `Entailment.Consistent T`, itself derived from
-- `RepresentsComputations`.
-- The supporting layer of this file — `paperPrimeDecompose_all` / `_exs` /
-- `_reprAllTerm` / `_neg_reprAllTerm`, `paperTheoryDP_covers_representedClaim(_neg)`,
-- `representedClaimSentence`, `representedClaimSentence_bigSentenceCodes`,
-- `provable_subst_binNumeral_iff`, `provable_reprAllTerm_binNumeral_iff` and its negated
-- form, `boundedArg`, `boundedArg_digits`, `universalRunValue`,
-- `universalRunValue_boundedArg`, `universalRunValue_computable`,
-- `representedBoundedClaims`, `exists_reprAll_of_representsComputations`,
-- `representedBoundedHaltingClaims`, and the two anti-vacuity witnesses above — is
-- axiom-clean but carries no `Paper node:` line, so it is covered transitively by the
-- endpoints named here rather than listed.
--
-- The **unbounded** halting lane (`thm:halts`, `thm:loops`) lives here too, and takes
-- `[Entailment.Consistent T]` rather than `[RepresentsComputations T]`: the positive
-- literal is Σ₁-completeness alone (`re_complete_mp`), and the negative literal is
-- `thm:loops`'s own `hloops` hypothesis, so representability is not needed.  The day-`n`
-- claim is `haltingArgClaimSentence machines inputs n`, the fixed universal schema at the
-- compact name of `⟨⌜mₙ⌝, xₙ⟩`, and `hloops` is stated at its bare arithmetic instance
-- `haltingArgClaimInstance machines inputs n` — the literal negation of the very sentence
-- whose atom the conclusion is about.  The public atom is a vacuous `∃⁰` wrapper whose
-- invisibility is proved rather than assumed (`provable_schemaArgClaim_iff`,
-- `provable_neg_schemaArgClaim_iff`).
-- Supporting declarations of this lane — `schemaArgClaim`, `schemaArgClaimSentence`,
-- `schemaArgClaimSentence_bigSentenceCodes`, `paperPrimeDecompose_schemaArgClaim(_neg)`,
-- `provable_iff_of_realize_iff`, `paperTheoryDP_covers_schemaArgClaim(_neg)`,
-- `haltingArgClaimSentence`, `haltingArgClaimInstance`, `haltingArgClaimInstance_true_iff`
-- — are axiom-clean and carry no `Paper node:` line, so they are covered transitively here
-- rather than listed.
--
-- The **§4.10 `Con` lane** (`thm:pac`, `thm:pazfc`) has a supporting layer of its own, held
-- to the same rule as the two lanes above and enumerated here for the same reason — every
-- one of these is an internal `def`/`lemma` carrying no `Paper node:` line, which
-- `scripts/check-paper-nodes.sh` forbids in an `#assert_axioms_clean` block, so they are
-- **covered transitively** by the two annotated endpoints listed below and axiom-checked by
-- the `#print axioms` block at the foot of `ComputationRepresented.lean`:
-- `conClaimArg`, `conClaimArg_digits`, `conClaimSentence`,
-- `conClaimSentence_bigSentenceCodes`, `conClaimSentence_ne_of_day_ne`,
-- `exists_reprAll_conRunValue`, `conGamma`, `conGamma_spec`, `representedConClaims`, and
-- the occurrence-discharge family added in R7 — `conGamma_mentions_zero`,
-- `conGamma_mentions_zero_of_bProv`, `conGamma_mentions_zero_of_horizon_unbounded`,
-- `conGamma_mentions_zero_ackermann` — together with the general lemma they rest on,
-- `mentions_zero_of_repr_ne` (`Framework/RepresentsComputations.lean`).
-- That family closes a claimed boundary that turned out not to be one (R7-B1): the
-- occurrence side condition `γ.Mentions 0`, which the docstrings here previously asserted
-- could **not** be discharged from the representation spec, IS derivable from it whenever
-- the represented decider is non-constant.  The counterexample that motivated the old
-- wording — a horizon constantly `0`, at which the decider is constant and a `γ` ignoring
-- its argument represents it correctly — bounds the claim to constant deciders only.  Every
-- unbounded horizon, the paper's own `Ack` included, is on the other side.
--
-- The **§4.10 `thm:incons` lane** likewise.  As of tranche 10 that lane is stated at the
-- paper's own subject matter — an arbitrary e.c. sequence of **recursively axiomatizable**
-- theories — and the deduction-family paraphrase is **retired**, not paraphrased differently.
-- `theoryOf m` is the theory whose axioms are the sentences whose written sources the machine
-- `m` enumerates; the endpoint's premises are the paper's own two and no others,
-- `hm : DigitMachineCodes m` (`def:ec` on the *naming*, the same write-out class `thm:halts`
-- uses for machines) and `hinc : ∀ n, ¬Consistent (theoryOf (m n))`.  Gone from the signature:
-- the base theory `T'`, its `[T'.Δ₁]` instance, the adjoined-axiom sequence `σ`, its source
-- `s`, the emission premise `hs` and the compilation bridge `hcompile`.
--
-- The uniformity is bought by **compactness**, not by an internal uniform-in-theory
-- derivability predicate — which Foundation cannot host, and that obstruction (9b) still
-- stands verbatim; this design sidesteps it rather than contradicting it.  Inconsistency is
-- always witnessed by finitely many axioms (`exists_inconsistent_list`, from the axiom list
-- Foundation's own proof object carries), a finite list of written axioms splices into one
-- written conjunction (`combineTokens`/`combineSourceNats`,
-- `Construction/Witnesses/SourceWindow.lean`), and refuting that conjunction is a question of
-- pure logic — so the represented predicate `MachineTheoryInconsistent` runs over the **empty
-- theory** (`Theory.Δ₁.empty`) and mentions no base theory at all.  It is r.e. because its
-- matrix is decidable (`proofPacked_computable ∅`), by `Partrec.rfind`/`Partrec.dom_re`;
-- Mathlib has no r.e.-projection lemma and none is used.
--
-- The supporting layer, none of it annotated.  **Two coverage classes, distinguished** — the
-- note here used to claim all of it was "covered transitively by the endpoint", which was
-- false by construction for half of it (R11-B1/B2):
--
--  (i) declarations the endpoint's own proof term *uses* really are covered transitively by
--      `lic_disbelief_inconsistent_theories_unconditional` below;
-- (ii) the day-machine write-out layer and the two applied witnesses are **not**: the
--      endpoint is universally quantified over `m`, so its proof term names no machine
--      family and no transitive check can reach a downstream application.  They are covered
--      instead by asserting the two applied witnesses directly — their *statements* name
--      `deepDayMachine` / `infiniteDayMachine` / `digitMachineCodes_dayMachine`, so the whole
--      `DayMachine.lean` layer is genuinely transitive through them — in the dedicated
--      `#assert_axioms_clean` block below.  The precedent is
--      `#assert_axioms_clean loopsTheory thm_loops_applied_at_loopsTheory` on the `thm:loops`
--      lane.  The same block asserts `machineTheoryInconsistent_iff`, the R11 faithfulness
--      bridge, which likewise no endpoint's proof term reaches.
--
-- Everything in both classes is additionally axiom-checked by the `#print axioms` blocks at
-- the feet of `ComputationRepresented.lean`, `SourceWindow.lean`, `SourceRecognizer.lean` and
-- `DayMachine.lean`.
--
-- Covered transitively by the endpoint:
-- `theoryOf`, `mem_theoryOf`, `not_consistent_of_refutable_mem`, `exists_window`,
-- `negSourceFormulaCode_sourceNat_of_sentence`, `negWindowCode_eq_quote`,
-- `MachineTheoryInconsistent`, `machineTheoryInconsistent_re`, `inconsistencySchema`,
-- `inconsistencySchema_spec`, `machineTheoryInconsistent_of_not_consistent`,
-- `not_machineTheoryInconsistent_of_diverges`, `evaln_neverHaltMachine`, `falsumSource` and
-- its two lemmas, `not_consistent_theoryOf_falsumMachine`,
-- `inconsistencySchema_not_argument_insensitive`, `inconsistencySchema_mentions_zero`,
-- `machineArg`, `inconsistencyArgClaimSentence`, `inconsistencyArgClaimInstance`,
-- `inconsistencyArgClaimSentence_ne_of_arg_ne`, `representedInconsistentTheoryClaims`; the
-- shared substrate `listConj`, `consistent_empty`, `exists_inconsistent_list`,
-- `provable_neg_listConj_of_not_consistent`, `provable_listConj`, `not_provableCode_zero`
-- (`Framework/BoundedConsistency.lean`), the gated token splice
-- (`Construction/Witnesses/SourceWindow.lean`) and the source recognizer it gates on
-- (`Construction/Witnesses/SourceRecognizer.lean`).
--
-- **Downstream of the endpoint, hence covered through the block asserted below rather than
-- through the endpoint** — the R11 converse chain
-- (`exists_source_of_sourceRun`, `exists_source_of_admissibleName`, `exists_source_gateName`,
-- `exists_sources_axiomWindow`, `not_consistent_theoryOf_of_machineTheoryInconsistent`, all
-- reached by `machineTheoryInconsistent_iff`, and
-- `ArithSource.compile_eq_of_sourceTokens_eq`, reached by both it and
-- `theoryOf_const_ofNNF`); and the
-- day-machine write-out layer (`Construction/Witnesses/DayMachine.lean`, whose
-- `BigDigits.ofBase16PolySegStream` is re-homed to `Framework/CodeSource.lean` beside its
-- base-64 twin) and the two applied witnesses
-- (`deepInconsistentSource`, `deepInconsistentAxiom`, `compile_deepInconsistentSource`,
-- `deepInconsistentSource_polyArithmeticSourceSeq`,
-- `sourceTokens_deepInconsistentSource_length`, `primrec_deepInconsistentSourceNat`,
-- `deepSourceCode`, `deepSourceCode_eval`, `provable_neg_deepInconsistentAxiom`,
-- `deepDayMachine`, `deepDayMachine_eval`, `deepInconsistentAxiom_mem_theoryOf`,
-- `not_consistent_theoryOf_deepDayMachine`, `thm_incons_applied_deep`,
-- `inconsistencyArgClaimSentence_deep_ne`, `infiniteDayMachine`, `infiniteDayMachine_eval`,
-- `deepInconsistentAxiom_mem_theoryOf_infinite`, `deepInconsistentAxiom_injective`,
-- `infinite_theoryOf_infiniteDayMachine`, `not_consistent_theoryOf_infiniteDayMachine`,
-- `thm_incons_applied_infinite`).
--
-- **No charge stands on that row.**  Both former charges are retired: the over-strength
-- `def:ec` premise `hσ : BigDigits (deductionFamilyArg σ)`, which metered a formula's Gödel
-- code (tranche 9-pre — see the WRITE-OUT FIELD MIGRATION block below), and now the
-- deduction-family paraphrase itself.  What remains is the global `[T.Δ₁]` / `[𝗣𝗔⁻ ⪯ T]`
-- disclosure on the **market's** theory, which is charged once globally and not against this
-- node, plus the stated presentation convention `dd:machinetheory` (what it means for a
-- machine to present a theory), which is a convention rather than a substitution — as
-- `dd:symbolcount` is — and is disclosed at the section header and in the glossary.
--
-- **R11 window repair (the sentence now matches the convention exactly).**  The audit found
-- the ungated window *unsound* against `dd:machinetheory`, in three independent ways:
-- `tokensOfNat` stops at the first sentinel, so numbers that are no name at all decode like
-- shorter names; the token splice is list surgery, so two *incomplete* runs concatenate into
-- one complete refutable run; and a genuine source may compile to a formula with free
-- variables, which pure logic can refute without it being a sentence of any theory.  Each
-- made `MachineTheoryInconsistent` hold of machines whose `theoryOf` is *empty*.  The repair
-- is a per-entry gate (`AdmissibleName`, `gateName`,
-- `Construction/Witnesses/SourceWindow.lean`): a number is admitted only if it is literally
-- the name of its own decoded run and that run is the complete emitted run of one
-- `ArithSource 0` whose compiled form is a sentence, certified by the new depth-tracking,
-- free-variable-rejecting recognizer `sourceRun`
-- (`Construction/Witnesses/SourceRecognizer.lean`, with `exists_source_of_sourceRun` its
-- soundness and `sourceRun_sourceTokens` its completeness).  **The endpoint's signature is
-- unchanged** and no premise moved; what changed is that the day-`n` sentence's content now
-- *equals* the convention's claim rather than being implied by it —
-- `machineTheoryInconsistent_iff` proves both directions, where before only
-- `machineTheoryInconsistent_of_not_consistent` held and its converse was false.  The
-- surjectivity justification is likewise scoped to what is proved: `theoryOf_const_ofNNF`
-- realizes every one-axiom theory exactly; the *uniform* enumeration half is stated as not
-- formalized, and is not consumed by the endpoint.
--
-- The anti-extensionality lemma **got stronger in the same change**:
-- `inconsistencySchema_mentions_zero` now has **no hypothesis at all**, where the
-- deduction-family version required `Entailment.Consistent Θ₀` (over an inconsistent base the
-- old provability predicate was extensionally constant and the schema could ignore its
-- argument).  The new represented predicate is non-constant outright — the machine that keeps
-- writing `⊥` presents an inconsistent theory, the machine that never writes presents the
-- empty one — so `inconsistencyArgClaimSentence_ne_of_arg_ne` is unconditional too.
--
-- Retired with the paraphrase, in collapsed form (no ₙ-suffixed layer, no parallel lane):
-- `deductionFamilyArg`, `falsumSource_polyArithmeticSourceSeq`, `provableCode_negSource_re`,
-- `deepInconsistentSource_sourceNat_ne`, `deepInconsistentAxiom_inconsistent`, and the
-- one-line `⊥`-adjunction `example`.  `provableCode_neg_iff_not_consistent_adjoin`
-- (`Framework/BoundedConsistency.lean`) loses its consumer on this lane and is kept only as
-- the deduction-theorem bridge it was; `deepInconsistentSource_sourceNat_ne` is replaced by
-- `dayMachine_sourceNat_ne`, which separates days by the *machine's* source rather than the
-- axiom's, because that is what the day-`n` sentence now writes out.  Earlier retirements on
-- this lane, recorded here for continuity: `alternatingInconsistentAxiom` and its family, and
-- `deductionFamilyArg_ne_of_ne` (R7).
--
-- What the new rendering buys that the old could not state: `thm_incons_applied_infinite`
-- exhibits day-theories with **infinitely many** axioms (`infinite_theoryOf_infiniteDayMachine`
-- — a deduction family adjoins one sentence and can never do this), each axiom having
-- `≥ 2 ^ k` nodes in normal form, all named by machine sources of `O(n)` symbols.
-- `thm_incons_applied_deep` keeps the finite analogue of the retired witness and is the one
-- that exercises the metering gap: the day machine's source is short, its single axiom is
-- `(∀x. A(x) ⟺ ⋯ ⟺ A(x)) ∧ ⊥`, and nothing about that axiom is metered because the paper
-- meters only the naming (tex:1931: "the runtime of an individual `mₙ` is immaterial").
--
-- Asserted here because the endpoint below cannot reach any of them: it is universally
-- quantified over `m`, so its proof term names no machine family and no transitive check
-- touches a downstream application, and `machineTheoryInconsistent_iff`'s new half is
-- consumed by nothing the endpoint proves.  The two witnesses carry the whole
-- `DayMachine.lean` layer with them, by naming it in their statements.
#assert_axioms_clean
  machineTheoryInconsistent_iff theoryOf_const_ofNNF
  thm_incons_applied_deep thm_incons_applied_infinite

#assert_axioms_clean
  DigitMachineCodes.computable ComputableHorizon.computable
  lic_does_not_anticipate_halting_ofComputation
  lic_belief_finitistic_consistency_unconditional
  lic_belief_stronger_theory_consistency_unconditional
  lic_does_not_anticipate_halting_unconditional
  lic_learns_halting_patterns_ofComputation
  lic_learns_provable_nonhalting_patterns_ofComputation
  lic_disbelief_inconsistent_theories_unconditional

-- Construction/Witnesses/LUVArithmetic.lean, LUVDeductiveProcess.lean — the LUV threshold
-- lane, migrated off soundness.  Both threshold literals are now taken over ONE sentence
-- (`thresholdSchema` and its literal negation) at the representability premise, so the LUV
-- provability world `luvWorld` is consistent by `Entailment.Consistent T` rather than by a
-- semantic argument.
-- Not inventoried yet, again for want of `Paper node:` lines:
-- `ComputableLUV.thresholdValue_computable`, `.thresholdGamma_spec`,
-- `.thresholdSchema_subst`, `.threshold_provable`, `.threshold_refutable`,
-- `.luvWorld_consistent`, `.luvThresholdDP_hworld`.  The `ArithmeticLUVPresentation`
-- freeze below is the Tier-2 record of this lane's field surface.

-- Construction/Witnesses/ComputationRepresented.lean — the N+ witness for `thm:loops`'s
-- refutation
-- premise `hloops`, which had none (2026-08-28 audit, R2-F17).  `loopsTheory` is `𝗜𝚺₁` plus
-- one *true* Π₁ axiom.  That axiom is the literal negation of the endpoint's own claim
-- sentence at the witness family:
-- `loopsWitnessSentence = ∼(haltingArgClaimInstance (fun _ => neverHaltMachine) (fun _ => 0) 0)`.
-- It is a *single* sentence rather than the `∀`-closure the previous rendering needed,
-- because the witness machine family is constant — the machine, not the day, is what left
-- the schema — so `loopsTheory_refutes` is plain `Entailment.by_axm` with no specialization
-- step.  The theory is `Δ₁` and consistent (both
-- fall out of every axiom being true in `ℕ`), and the machines it speaks of provably never
-- halt, so the endpoint's `≈ₙ 0` conclusion is the semantically correct one.  It is also
-- Σ₁-sound, but that is now only a record of the witness's quality:
-- `lic_learns_provable_nonhalting_patterns_unconditional` takes no soundness instance any
-- more, so `loopsTheory_soundOnSigma1` is consumed by nothing the endpoint asks for.
-- `thm_loops_applied_at_loopsTheory` applies the endpoint with every instance and every
-- hypothesis discharged.  **The refutation holds by axiom fiat, not by arithmetic
-- reasoning** — the disclosure at `loopsTheory` records why the slot is **unreachable with
-- the installed substrate**, which is a weaker and more accurate claim than the one this
-- note carried before (2026-08-28 audit, R3-F01/R3-F12).  What is *not* true is that no
-- natural theory could refute a false halting instance: refuting a false Σ₁ sentence is
-- proving a true Π₁ one, which Σ₁-soundness permits, and the uniform
-- `incomplete_of_REPred_not_ComputablePred_Nat'` constrains no single instance — `𝗜𝚺₁`
-- would refute a natural arithmetization of `rfind' succ` diverging by trivial induction.
-- The actual obstruction is representational, and the R5-F08 repair does not touch it: the
-- endpoint's schema is `universalHaltingSchema = codeOfREPred UniversalCodeHalts`, and
-- Foundation picks that formula by `Classical.epsilon`
-- (`R0/Representation.lean:232-247`), so its *shape* is unreachable from the API and nothing
-- about it can be proved beyond its defining spec, which is a statement about standard-model
-- truth; the only lemmas carrying that to `T ⊢ …` are the positive ones.  The disclosure at
-- `loopsTheory` names two honest strengthenings — a Π₁-reflection hypothesis on `T`, or a
-- hand-rolled Δ₀/Σ₁ halting formula carrying its own representability lemma; a
-- `halting_fails` field on `ComputationTheoryPresentation` would be a third.
-- The *bounded* half of that gap is now closed by the paper's own premise rather
-- than by any of them: `boundedFailure_refutes` takes the literal negation of the
-- bounded-halting sentence, supplied by `RepresentsComputations`, so the retired
-- `universalBoundedFailureSchema` apparatus is gone and `theoremDP_hworld`'s tag-3 case
-- closes from consistency; tag 7 closes the same way as of 2026-08-30 (one `code` formula,
-- two value fibers — see the `BooleanQuoteCode` block below).  The *unbounded* half — `thm:loops`'s `hloops`, a Π₁ refutation
-- of a non-halting instance — is not, and is what `loopsTheory` still witnesses by axiom.
-- `loopsTheory_refutes` is deliberately *not* inventoried: it is the internal
-- premise-discharge step (`Entailment.by_axm`), not a paper claim, so it carries no
-- `Paper node` line and is covered transitively by the applied endpoint below.
#assert_axioms_clean
  loopsTheory
  thm_loops_applied_at_loopsTheory

-- Construction/Witnesses/QuoteCodeOfMarket.lean (market-generic parts) and
-- Construction/Witnesses/PaperMarket.lean (the instantiations at the single market
-- `paperDP`) — constructed rational quote codes: the first *discharge* of the
-- `RationalQuoteCode` reflection data.  `lic_expectations_of_probabilities_closed` is
-- `thm:epr` over the constructed LIA with no reflection hypotheses at all.
#assert_axioms_clean
  arithmeticThresholdLUV_polyThresholdCodeSeq
  RationalQuoteCode.ofComputable
  MarketComputation.expectQuote_computable
  paperPriceQuoteCode paperExpectationQuoteCode
  lic_expectations_of_probabilities_closed
  lic_iterated_expectations_closed

-- The deferred-day / self-trust reflection data constructed from the market
-- program.  `indicatorProductLUV_valuesAt` is the product law behind `thm:st`'s `A`.
-- `PGenerableRat.computable` is the certification that lets the closed quote codes emit a
-- threshold sentence about a *P-generable* (`def:ece`) threshold: parse the feature back
-- out of its emitted serialization, evaluate it against the certified market, minimize
-- over the interpreter clock.
#assert_axioms_clean
  paperFutureQuoteCode paperDeferredExpectationQuoteCode
  paperConfidenceQuoteCode
  PGenerableRat.computable
  indicatorProductLUV_valuesAt indicatorProductLUV_bigThresholdCodeSeq
  lic_no_expected_net_update_closed
  lic_expected_future_expectations_closed
  lic_self_trust_closed
  paperIntervalQuoteCode lic_introspection_closed

-- Historical mesh `ccee`: the weighted conditional, **general-source** closed form. The deferred-weight
-- quote code names the `w ∘ f` program (deferral costs nothing at emission), and
-- `meshProductLUV` renders the product from that quote's own threshold atoms on a
-- width-`n+1` mesh, so no emitter ever needs the value `w (f n)` (which is neither
-- available — P-generable, and deferred — nor polynomially sized).  The price is that the
-- left product reflects only to within `1/(n+1)`: a **disclosed type-`(c)` substitution**
-- carried by `ConditionalExpectationQuote.slack`.  `indicatorProductLUV_exact_left_reflected`
-- is the non-vacuity witness at the exact (`slack = 0`) end.  See the Part F header and the
-- README's modeling-boundary history.  This is the **general-input** `thm:ccee` form: it
-- admits an arbitrary threshold-only e.c. source, and pays the mesh for it.  The exact
-- same-market endpoint for the paper's *literal* sources is audited two blocks down.
#assert_axioms_clean
  PCWorld.ValuesAt.eq
  theoremDeferredWeightQuoteCode paperDeferredWeightQuoteCode
  paperConditionalExpectationQuoteCode
  meshProductLUV_valuesAt
  meshProductLUV_rpnThresholdCodeSeq
  indicatorProductLUV_exact_left_reflected
  lic_no_expected_net_update_conditional_closed

-- Construction/Witnesses/PaperExactProduct.lean, PaperRepresentedWeight.lean,
-- PaperExactCCEE.lean — the exact `thm:ccee` endpoint **on the single market**.
--
-- A `PaperLUV` names its value by a numerator/positive-denominator pair code, so two of
-- them multiply exactly inside arithmetic: `paperProductPaperLUV` is the unreduced product
-- code `(a·c)/(b·d)`, and `paperProductPaperLUV_valuesAt` proves its rational cut is
-- exactly the product of the factors' cuts.  The deferred weight is represented literally
-- by `RepresentsComputations` (the paper's own §2 premise on `Θ`), so nothing has to name
-- the value `w (f n)` as a numeral.  The deductive process is untouched: the endpoint is
-- stated over `liaHistory (paperDP T)` like every other canonical endpoint, at `slack = 0`.
#assert_axioms_clean
  PaperLUV.paperProductPaperLUV
  PaperLUV.paperProductPaperLUV_valuesAt
  paperExactProductLUVSeq
  representedPairPaperLUV
  representedPairPaperLUV_valuesAt
  representedPairPaperLUVSeq
  deferredWeightPaperLUVSeq
  deferredWeightPaperLUVSeq_valuesAt
  lic_no_expected_net_update_conditional_paperLUV_ofWeightSeq
  lic_no_expected_net_update_conditional_paperLUV_closed

-- Construction/Witnesses/SemanticLiftedCCEE.lean — the generalized semantic-extension form
-- of `thm:ccee`, retained but no longer the canonical paper rendering.
-- A fixed old-language copy prevents semantic self-reference; finite-stage entailment
-- admits every source satisfying the paper-facing `source_valued` premise, including
-- threshold-only ones that are not literal paper LUVs. The one canonical process is fixed
-- from `T`, has an explicit completed world, and supports the exact semantic product with
-- zero slack — at the cost of pricing in `liaHistory (canonicalCCEEDP T)` rather than the
-- single market.
#assert_axioms_clean
  liftedCCEEBaseDP_computable
  liftedCCEEBaseWorld_hworld
  canonicalCCEEDP_computable
  canonicalCCEEDP_hworld
  liftedRpnSemanticHandle_valuesAt
  liftedRpnSource_factor_eventually
  canonicalRationalQuote_factor_eventually
  lic_no_expected_net_update_conditional_exact_canonical

-- Construction/Witnesses/ProductDefinition.lean — the exact-reflection route for the quoted
-- product.  Fresh product atoms are defined by the deductive process itself (a definitional
-- extension of the *process*, not of the theory), so a completed world values the product at
-- exactly `x · w` — `slack = 0`, no positivity hypothesis on the weight.
--
-- This historical diagnostic does **not** carry the `thm:ccee` row, and is inventoried so
-- its axiom cleanliness is gated. The endpoint of record is now the fixed-language
-- construction `lic_no_expected_net_update_conditional_exact_canonical` above.
--
-- The route reaches a closed statement, `lic_no_expected_net_update_conditional_exact_productExtension`:
-- exact reflection over the constructed `LIA` on `theoremDP T ∪ productDefDP`, with `hworld`,
-- `source_valued`, `weight_valued` and `right_reflected` all discharged, and a jointly
-- satisfiable premise set exhibited by `..._nonvacuous`.  Its role is **diagnostic**, not
-- paper-facing: it shows the mesh endpoint's slack is an artifact of the propositional
-- substrate rather than of logical induction, because the same trader and criterion give an
-- exact conclusion once the product exists syntactically.
--
-- It establishes nothing about the base inductor's conditional expectations: `LIA` over the
-- extended process is a different inductor, and conservativity of completed-world truth does
-- not carry prices across.  This was adjudicated cross-family on 2026-08-11 (rejecting the
-- reading of it as `thm:ccee` at an instance; ranking mesh > this > weight-narrowing), and
-- the two costs it carries and the mesh endpoint does not — a genuine freshness restriction
-- on the source class, and `def:pgen` at the extended market — are stated at the theorem, in
-- `LogicalInduction/README.md` and in `scripts/coverage-classification.md`.  Full assessment
-- and the adjudication outcome in `LogicalInduction/notes/boundary-propositional-substrate.md`.
#assert_axioms_clean
  productDefDP_computable
  productDefDP_union_consistentWithTheory
  productLUV_valuesAt
  productLUV_valuesAt_union
  productLUV_rpnThresholdCodeSeq
  lic_no_expected_net_update_conditional_exact
  QuotationTheoryPresentation.mono
  exactProductDP_hworld
  lic_no_expected_net_update_conditional_exact_productExtension
  lic_no_expected_net_update_conditional_exact_productExtension_nonvacuous

-- Unconditional-over-LIA capstones
-- (parity with the paradox-resistance and conditioning `_unconditional` endpoints above).
-- The quotation family below discharges market/inductor/presentation/hworld; the
-- reflection data (`RationalQuoteCode`, `*_reflected`) stays a caller hypothesis here,
-- discharged where needed by `RationalQuoteCode.ofComputable` (QuoteCodeOfMarket.lean).
-- What `ComputationDP.lean` still owns is the presentation (`theoremPresentation`), the
-- quotation lane over `theoremDP` and `thm:incons`.  The halting lane is **not** here any
-- more: `lia_learns_halting_patterns_unconditional` and
-- `lic_learns_provable_nonhalting_patterns_unconditional` are stated in
-- `ComputationRepresented.lean` over `paperTheoryDP T` under
-- `[T.Δ₁] [𝗣𝗔⁻ ⪯ T] [Entailment.Consistent T]`, with no soundness instance and, since
-- tranche 7, no `[𝗜𝚺₁ ⪯ T]` either, as
-- `thm:pac` / `thm:pazfc` / `thm:dontwait` beside them already were.  They are listed here
-- because this block is the capstone roll-up, not because of where they live.
#assert_axioms_clean
  lia_learns_halting_patterns_unconditional
  lic_expectations_of_probabilities_ofCode_unconditional
  lic_iterated_expectations_ofCode_unconditional
  lic_introspection_ofCode_unconditional
  lic_expected_future_expectations_ofRepresentation_unconditional
  lic_no_expected_net_update_ofRepresentation_unconditional
  lic_no_expected_net_update_conditional_ofRepresentation_unconditional
  lic_self_trust_ofRepresentation_unconditional
  lic_belief_finitistic_consistency_unconditional
  lic_belief_stronger_theory_consistency_unconditional
  lic_disbelief_inconsistent_theories_unconditional
  lic_learns_provable_nonhalting_patterns_unconditional
  lic_does_not_anticipate_halting_unconditional


/-! ## Per-declaration axiom coverage

`scripts/check_endpoint_coverage.py` requires that **every** declaration under
`LogicalInduction/` carrying a `Paper node:` docstring line is named in some
`#assert_axioms_clean` block here.  The blocks above are grouped by paper node and carry
the tier notes; the blocks below close that rule for everything else — construction
machinery, emission certificates, applied witnesses and boundary structures that cite a
paper node as provenance without being that node's headline endpoint.

They are internal axiom regression assertions, not public trust surface: the public
canonical endpoint inventory is the `LI-CANONICAL` block alone.  They add no paper node,
so the tallies in `scripts/coverage-classification.md` and `LogicalInduction/README.md`,
which are per-*label*, are unchanged by anything here.  The reverse gate used to be
per-label too, and that was the hole: one asserted carrier satisfied a label, so a second
annotated declaration for the same label passed every checker while sitting under no
axiom gate.  A `#assert_fields` freeze does not close it either — it checks field names,
not axioms.  Grouped by defining file. -/

-- LogicalInduction/Framework/Affine.lean
#assert_axioms_clean
  AffineCombination.PolySequence

-- LogicalInduction/Framework/Criterion.lean
#assert_axioms_clean
  EfficientlyComputableDigit MarketComputation clockedTrader

-- LogicalInduction/Framework/Expectations.lean
#assert_axioms_clean
  LUV.RpnThresholdCodeSeq LUV.RpnThresholdCodes LUV.BigThresholdCodeSeq

-- LogicalInduction/Framework/RpnEmission.lean
#assert_axioms_clean
  EfficientlyComputable.ofDigitEmitter EfficientlyComputable.ofSingleTradeBlocks
  EfficientlyComputable.ofTokenEmitter IsLogicalInductor.noExploitDigit
  IsLogicalInductor.noExploitTok RpnSpliceStream.ec

-- LogicalInduction/Framework/RpnSplice.lean
#assert_axioms_clean
  RpnSentenceCodes RpnSentenceCodes.bigOr RpnSentenceCodes.bigAnd

-- LogicalInduction/Framework/WriteOut.lean
#assert_axioms_clean
  BigSentenceCodes BigSentenceCodes.bigAnd BigSpliceStream.ec BigTokenStream
  BigTokenStream.digitizeStream
  DigitRatCodes EfficientlyComputable.ofSingleTradeBlocksBig ec_of_bigTokenStream

-- LogicalInduction/Construction/TradingFirm.lean
#assert_axioms_clean
  trading_firm_dominance_of_ec

-- LogicalInduction/Construction/Witnesses/ArithmeticSource.lean
#assert_axioms_clean
  PaperLUVCombination PaperLUVSeq iffChainSource_polyArithmeticSourceSeq iffPaperLUV
  invPaperLUVWith

-- LogicalInduction/Construction/Witnesses/BoundedEvaluation.lean
#assert_axioms_clean
  CEEnumeration SettlementChecker

-- LogicalInduction/Construction/Witnesses/ComputationDP.lean
#assert_axioms_clean
  liaMarketComputation quotationPresentation quotation_presentation_nonvacuous

-- LogicalInduction/Construction/Witnesses/ComputationSyntax.lean
#assert_axioms_clean
  ComputableHorizon ComputationTheoryPresentation

-- LogicalInduction/Construction/Witnesses/ConditioningPresentation.lean
#assert_axioms_clean
  CompactConditioningProcessComputation

-- LogicalInduction/Construction/Witnesses/FeedbackTruth.lean
#assert_axioms_clean
  FeedbackTruth.FeedbackTruthComputation

-- LogicalInduction/Construction/Witnesses/FinitePerturbationWitness.lean
#assert_axioms_clean
  FinitePerturbationCounterexample.exists_advice_perturbation
  FinitePerturbationCounterexample.exists_advice_perturbation_ofTheory
  FinitePerturbationCounterexample.not_overgeneral_ifp_ofTheory

-- LogicalInduction/Construction/Witnesses/HistoricalMaturity.lean
#assert_axioms_clean
  AffineCombination.ApproxDeterminedViaTheory.lic_prandaff
  AffineCombination.ApproxDeterminedViaTheory.lic_prandaff_above
  AffineCombination.ApproxDeterminedViaTheory.lic_prandaff_below
  AffineCombination.DeterminedViaTheory.lic_prandaff
  AffineCombination.DeterminedViaTheory.lic_prandaff_above
  AffineCombination.DeterminedViaTheory.lic_prandaff_below

-- LogicalInduction/Construction/Witnesses/LUVArithmetic.lean
#assert_axioms_clean
  ComputableLUV ComputableLUV.toLUV ComputableLUV.toLUV_polyThresholdCodes

-- LogicalInduction/Construction/Witnesses/LUVPresentation.lean
#assert_axioms_clean
  ArithmeticLUVPresentation

-- LogicalInduction/Construction/Witnesses/LUVSyntax.lean
#assert_axioms_clean
  LUVCombinationSyntax

-- LogicalInduction/Construction/Witnesses/PrefixMachine.lean
#assert_axioms_clean
  approx_polyRat_of_sentence dcStep natCode prefixApprox prefixKappa prefixKraft_of_code
  prefixMachinePresentation prefixSentenceEnum prefixThresholdEmission sentCode
  sentencePoly_of_invalidBit validCode

-- LogicalInduction/Construction/Witnesses/ProductDefinition.lean
#assert_axioms_clean
  exactProductDP exactWeightLUV productAtom_mesh_encode_polyFueled productDefDP
  productExtensionWorld_consistentWithTheory productExtensionWorld_holds_schema

-- LogicalInduction/Construction/Witnesses/QuotationAffine.lean
#assert_axioms_clean
  BooleanQuoteCode PairedWeighting ParameterizedDiagonalQuoteCode
  QuotationTheoryPresentation RationalQuoteCode

-- LogicalInduction/Construction/Witnesses/QuoteCodeOfMarket.lean
#assert_axioms_clean
  conditionalExpectationQuoteCode deferredWeightQuoteCode ordinaryLUVCombinationSeq
  quoteAtom_mesh_encode_polyFueled

-- LogicalInduction/Construction/Witnesses/RpnConditioning.lean
#assert_axioms_clean
  RpnConditioning.depthMode_unRpn_agree RpnConditioning.frameAgree_unRpn_rpnFrameOutput
  RpnConditioning.frameContract_rpnFrameOutput
  RpnConditioning.frameJoint_unRpn_rpnFrameOutput RpnConditioning.rpnFrameEmit_contractsTo
  RpnConditioning.rpnFrameOutput_polySegStream
  RpnConditioning.rpnGuardedConditionRun_polySegStream_of
  RpnConditioning.strategyOfTokens_unRpn_rpnFrameOutput_trades
  RpnConditioning.strategyOfTokens_unRpn_trades_eq_nil_of_rpnBigDay
  RpnConditioning.tradeRuns_unRpn_agree RpnConditioning.unRpn_rpnConditionRun_of
  RpnConditioning.unRpn_split

-- LogicalInduction/Construction/Witnesses/StrictSeparators.lean
#assert_axioms_clean
  exists_pos_mass_of_ce_nested

-- LogicalInduction/Construction/Witnesses/UniversalDovetailer.lean
#assert_axioms_clean
  Dovetail.dovetailMass Dovetail.dovetailMass_eq_mass Dovetail.dusApprox
  Dovetail.lowerSemicomputable Dovetail.rawVal Dovetail.trim_tendsto_of_exact
  Dovetail.universalApprox Dovetail.universalMass

-- LogicalInduction/Construction/Witnesses/UniversalPrefix.lean
#assert_axioms_clean
  UPrefix.UHalt UPrefix.kappaStage UPrefix.kappaU UPrefix.uCode UPrefix.uMinLen
  UPrefix.uSel

-- LogicalInduction/Properties/Conditioning.lean
#assert_axioms_clean
  ConditioningPresentation ConditioningTraderCompiler EventualConditioningFloor
  EventualConditioningOperationalWitness GatedConditioningOperationalWitness
  Trader.conditionedTranslation_exploits_base
  Trader.eventualConditionedTranslation_exploits_base

-- LogicalInduction/Properties/ExpectationProperties.lean
#assert_axioms_clean
  LUVCombination LUVCombination.ExactTheoryPresentation
  LUVCombination.MeshSoftmaxOperationalWitness LUVCombination.PolySequence

-- LogicalInduction/Properties/FinitePerturbationCounterexample.lean
#assert_axioms_clean
  FinitePerturbationCounterexample.not_overgeneral_ifp_of_advice

-- LogicalInduction/Properties/FinitePerturbations.lean
#assert_axioms_clean
  EfficientPrefixPatch FiniteSupportPatch MachineFiniteSupportPatch
  machineFiniteSupportPatch_of_rewriter

-- LogicalInduction/Properties/Introspection.lean
#assert_axioms_clean
  CompletedAffineQuoteApprox CompletedAffineQuoteEq CurrentExpectationQuote
  CurrentPriceExpectationQuote IntrospectionIntervalQuote ParadoxResistanceQuote

-- LogicalInduction/Properties/LimitCoherence.lean
#assert_axioms_clean
  gaifmanMeasure_sentence gaifmanWorldMeasure_sentence lic_gaifmanMeasure_supported
  lic_gaifmanWorldMeasure_supported lic_limitingBelief_gaifman

-- LogicalInduction/Properties/MetaLearning.lean
#assert_axioms_clean
  InconsistentTheoryClaims RepresentedDecidableClaims RepresentedSemidecidableClaims

-- LogicalInduction/Properties/OccamBounds.lean
#assert_axioms_clean
  OccamThresholdEmission PrefixMachinePresentation PrefixNegationCompiler

-- LogicalInduction/Properties/ProvabilityInduction.lean
#assert_axioms_clean
  buySeq_ec_big

-- LogicalInduction/Properties/Pseudorandomness.lean
#assert_axioms_clean
  AffineCombination.FeedbackTraderEmission AffineCombination.FeedbackTraderEmissionFamily
  AffineCombination.FeedbackTraderEmissionSigns AffineCombination.FeedbackTruthSequence
  PatientSettlementClock PseudorandomFrequencyInfrastructureWithHistoricalVerifiers
  lic_learning_pseudorandom_frequency_above_of_historicalVerifiers
  lic_learning_pseudorandom_frequency_below_of_historicalVerifiers
  lic_learning_pseudorandom_frequency_of_historicalVerifiers
  lic_learning_varied_pseudorandom_above_of_historicalVerifiers
  lic_learning_varied_pseudorandom_below_of_historicalVerifiers
  lic_learning_varied_pseudorandom_of_historicalVerifiers

-- LogicalInduction/Properties/SelfTrust.lean
#assert_axioms_clean
  AffineQuoteEq AffineQuoteGE AffineQuotePortfolio ConditionalExpectationQuote
  ExpectedFutureExpectationQuote FuturePriceQuote SelfTrustQuote

-- LogicalInduction/Properties/UniformNonDogmatism.lean
#assert_axioms_clean
  EfficientRepeatedEnumeration obuTrader_ec

-- LogicalInduction/Properties/UniversalSemimeasure.lean
#assert_axioms_clean
  BitPrefixSentences ContinuousSemimeasure DUSApproximationPresentation
  DUSThresholdEmission IndependentBitAtoms LowerSemicomputableContinuousSemimeasure
  StrictSeparatorPresentation UniversalContinuousSemimeasure


open AffineCombination LUVCombination in
/-! ## Tier-2 boundary structures — field (hypothesis) surface

Each structure below appears in the *type* of a Tier-1 endpoint (directly, or
transitively through structure fields), so its fields are hypotheses the statement
read-through must audit. `#assert_fields` freezes that field-name set: adding or removing
a field — smuggling a premise in or out of a boundary — fails the build. It does not
freeze field *types* (see the macro's docstring); deliberate type changes are recorded in
comments beside the affected structure. The set is order-insensitive. Regenerate with
`SurfaceProbe`/`FieldProbe` if the surface changes deliberately. -/

#assert_fields AffineCombination
  const terms
#assert_fields AffineCombination.BoundedCombinationSequence
  poly bounded
#assert_fields AffineCombination.FeedbackTraderEmission
  tradeCount coefficient sentence tradeCount_poly coefficient_poly sentence_poly trades_eq
#assert_fields AffineCombination.FeedbackTraderEmissionFamily
  emit
#assert_fields AffineCombination.FeedbackTraderEmissionSigns
  positive negative
#assert_fields AffineCombination.FeedbackTruthSequence
  determined sequence poly bounded magnitude value_vanishing feedback_price
#assert_fields AffineCombination.PolySequence
  termCount coefficient sentence termCount_poly const_poly coefficient_poly sentence_poly terms_eq const_rank coefficient_rank const_closed coefficient_closed
#assert_fields AffineQuoteEq
  toAffineQuotePortfolio future_coherent
#assert_fields AffineQuoteGE
  toAffineQuotePortfolio future_coherent
#assert_fields AffineQuotePortfolio
  family poly scale scale_pos current_price bounded magnitude_le_one
-- TYPE CHANGE, invisible to `#assert_fields` (which freezes field *names* only).
-- `ArithmeticLUVPresentation` now carries an `[RepresentsComputations T]` instance binder,
-- and its two fields are the two literals over ONE sentence:
--     threshold_enters  : T ⊢ (L.thresholdSchema T)/[code]      → …
--     threshold_refutes : T ⊢ ∼((L.thresholdSchema T)/[code])   → …
-- Previously `threshold_refutes` consumed a *second*, complementary r.e. schema
-- (`L.thresholdFailureSchema`, now retired), which is why the LUV world needed
-- Σ₁-soundness.  See `LUVArithmetic.lean`, "The threshold schema, at the paper's
-- representability premise".
#assert_fields ArithmeticLUVPresentation
  threshold_enters threshold_refutes
-- Tier-2 field change (2026-07-30, superseded 2026-08-28): `prefix_codes` moved from the
-- whole-value `PolySentenceCodes` to the token-metered `RpnSentenceCodes`, and then to the
-- write-out class `BigSentenceCodes` in the migration recorded in the WRITE-OUT FIELD
-- MIGRATION block below.  `#assert_fields` freezes field *names* only, so the type change is
-- recorded here explicitly; it is what makes the structure inhabitable
-- (`ordinaryBitPrefixSentences`).
#assert_fields BitPrefixSentences
  atom prefixSentence enumeration enumeration_covers prefix_codes holds_prefix realizable
-- TYPE CHANGE, invisible to `#assert_fields` (which freezes field *names* only).
-- The `pos_complete`/`neg_complete` fields of `BooleanQuoteCode` and `RationalQuoteCode`,
-- and `quote_positive_enters`/`quote_negative_refutes` of `QuotationTheoryPresentation`,
-- still read `T ⊢ universalQuotePos/[…]` / `T ⊢ universalQuoteNeg/[…]` — but those two
-- schemas are no longer two *independent* `codeOfREPred` Σ₁ formulas.  As of 2026-08-30
-- they are the value-`1` and value-`0` fibers of ONE Foundation `code` formula for the
-- universal quote evaluation (`universalQuoteCode`; `valueSchema`,
-- `Framework/QuoteRepresentability.lean`).  Field names and the printed field types are
-- unchanged, so the freezes below still pass, but the *content* is strictly different:
-- `T ⊢ ∼(pos/[w̄] ⋏ neg/[w̄])` is now provable (`universalQuote_exclusive_prov`, from the
-- locally revived `code_uniq` plus Gödel completeness under `𝗣𝗔⁻ ⪯ T`), where before the
-- fibers were separated only by truth in `ℕ`.  That is what retired `[T.SoundOnHierarchy
-- 𝚺 1]` from `theoremDP_hworld`'s tag 7 and from every endpoint downstream of it.
-- `quoteSchemas_exclusive_prov` is spelled `universalQuote_exclusive_prov` here and is
-- **not** inventoried: it is an internal exclusivity step, not a paper claim, so it carries
-- no `Paper node` line (`check-paper-nodes.sh` requires one of every inventoried name) and
-- is covered transitively by the quotation endpoints below.
#assert_fields BooleanQuoteCode
  code pos_complete neg_complete
#assert_fields CEEnumeration
  code halts outputs_sound
-- TYPE CHANGE, invisible to `#assert_fields` (which freezes field *names* only).
-- 2026-09-02: `condition_codes` moved from `RpnSentenceCodes` to `BigSentenceCodes`
-- (`def:ec`'s own write-out class) — a WIDENING of what a caller may supply, carried by
-- `BigTokenStream.digitizeStream` + `CondStep.machineSentenceBlocks_of_big`.  The field
-- name is unchanged, so this block passes without moving; the freeze does not see it.
#assert_fields CompactConditioningProcessComputation
  toDeductiveProcessComputation condition_codes
#assert_fields CompletedAffineQuoteApprox
  toAffineQuotePortfolio theory_coherent
#assert_fields CompletedAffineQuoteEq
  toAffineQuotePortfolio theory_coherent
#assert_fields ComputableHorizon
  program program_spec
-- TYPE CHANGE, invisible to `#assert_fields` (which freezes field *names* only).
-- `ComputationTheoryPresentation.boundedFailure_refutes` now consumes the LITERAL
-- NEGATION of the sentence its positive partner consumes:
--     boundedHalting_enters  : T ⊢ universalBoundedHaltingSchema/[↑z]    → …
--     boundedFailure_refutes : T ⊢ ∼(universalBoundedHaltingSchema/[↑z]) → …
-- Previously it consumed a *second*, independent r.e. schema
-- (`universalBoundedFailureSchema`, now retired), which is why `theoremDP_hworld`'s
-- tag-3 case needed Σ₁-soundness; it now closes from `Entailment.Consistent T` exactly
-- like tag 1.  Tag 7 (¬quotation) followed on 2026-08-30 by the same principle applied to
-- the quotation schemas — one `code` formula, two value fibers — so `theoremDP_hworld` now
-- reads `[T.Δ₁] [𝗣𝗔⁻ ⪯ T] [Entailment.Consistent T]` (tranche 7 replaced `[𝗜𝚺₁ ⪯ T]` with
-- the `𝗣𝗔⁻` the tag-7 case actually spends) and NO declaration in
-- `LogicalInduction/` carries a `SoundOnHierarchy` instance binder any more.
-- 2026-08-31 (T8/8, tag-space retirement).  The `inconsistency_enters` and
-- `inconsistency_refutesConsistency` fields are GONE, together with
-- `ComputationClaimKind.inconsistency`/`.consistency`, `inconsistencyClaim`/
-- `consistencyClaim` and their claim sentences: the T8/iv restatement moved `thm:incons`
-- onto `paperTheoryDP` (`representedInconsistentTheoryClaims`,
-- `ComputationRepresented.lean`), leaving those two rows of `theoremDP`'s tag table with
-- no consumer.  `theoremDP`'s event tag space is now `0`–`5` and gapless: `0`/`1`
-- halting ±, `2`/`3` bounded halting ±, `4`/`5` quotation ± (the quotation tags were
-- `6`/`7` before this change, and audit prose above and below dated earlier than
-- 2026-08-31 refers to them by those numbers).  `theoremDP_hworld` was re-established
-- over the shrunk space by deleting the two retired cases; the surviving cases are
-- unchanged, and no endpoint's elaborated signature moved.  The block below is shortened
-- by exactly the two retired field names.
#assert_fields ComputationTheoryPresentation
  theory_deltaOne process halting_enters halting_refutes boundedHalting_enters boundedFailure_refutes
#assert_fields ConditionalExpectationQuote
  weight_mem weight_generable source_codes left_codes right_codes slack slack_tendsto source_valued left_reflected right_reflected affine
-- TYPE CHANGE, invisible to `#assert_fields` (which freezes field *names* only).
-- 2026-09-02: `condition_codes` moved from `RpnSentenceCodes` to `BigSentenceCodes`, the
-- same widening recorded at `CompactConditioningProcessComputation` above.
#assert_fields ConditioningPresentation
  condition condition_codes holds_condition combined_computable
#assert_fields ConditioningTraderCompiler
  conditioned_computable translate translate_ec translate_machine tracks_on_condition
  preserves_floor
#assert_fields ContinuousSemimeasure
  mass nonneg root_le_one children_le
#assert_fields CurrentExpectationQuote
  source_codes quote_codes reflected affine
#assert_fields CurrentPriceExpectationQuote
  sentence_codes quote_codes reflected affine
#assert_fields DUSApproximationPresentation
  approximation nonneg le_mass tendsto
#assert_fields DUSThresholdEmission
  threshold_sum_codes inverse_width_codes
#assert_fields DeductiveProcess
  D mono
#assert_fields DeductiveProcessComputation
  code code_spec
#assert_fields DeferralFunction
  f lt code fueled
#assert_fields EfficientPrefixPatch
  quote quote_exact preserves_ec
#assert_fields FiniteSupportPatch
  quote quote_exact preserves_ec
#assert_fields EfficientRepeatedEnumeration
  sequence sequence_poly repeats sound covers
#assert_fields EventualConditioningFloor
  cutoff zeroDays zeroDays_lt epsilon epsilon_pos zero_exact positive_floor
#assert_fields EventualConditioningOperationalWitness
  floor conditioned_computable translation_ec translation_machine
#assert_fields ExpectedFutureExpectationQuote
  source_codes quote_codes reflected affine
#assert_fields FeedbackTruth.FeedbackTruthComputation
  value code a degree computes agrees
#assert_fields FuturePriceQuote
  sentence_codes quote_codes reflected affine
#assert_fields GatedConditioningOperationalWitness
  epsilon_pos denominator_floor conditioned_computable translation_ec translation_machine
#assert_fields GeneratedRatFeature
  rank_le polyTok closed denote
#assert_fields InconsistentTheoryClaims
  inconsistencySentence inconsistency_poly inconsistency_provable
#assert_fields IndependentBitAtoms
  atom realizable
#assert_fields IntrospectionIntervalQuote
  source_codes lower_feature lower_generated upper_feature upper_generated
  inverse_width_codes width_pos width_tendsto_zero probability_bounds quote
  quote_codes reflected inside_affine outside_affine
-- Both criteria are frozen. `IsMachineLogicalInductor` is `def:lic` at the paper's own
-- quantifier and is what the construction proves; `IsLogicalInductor` is the fuel-class
-- compatibility reading reached from it by `IsMachineLogicalInductor.toIsLogicalInductor`,
-- and is what the §4 tail is conditioned on. Freezing only the second left the canonical
-- criterion's premise set unguarded.
#assert_fields IsMachineLogicalInductor
  marketComputable processComputable noExploit
#assert_fields IsLogicalInductor
  marketComputable processComputable noExploit
#assert_fields MachineFiniteSupportPatch
  quote quote_exact preserves_ec
#assert_fields LUV
  gt
#assert_fields LUVCombination
  const terms
#assert_fields LUVCombination.BoundedSequence
  poly bounded
#assert_fields LUVCombination.ExactTheoryPresentation
  value value_mem threshold_iff
#assert_fields LUVCombination.MeshSoftmaxOperationalWitness
  poly bounded magnitude lower_poly lower_bounded lower_magnitude
#assert_fields LUVCombination.PolySequence
  mesh_poly
#assert_fields LUVCombinationSyntax
  termCount coefficient luv termCount_poly const_poly coefficient_poly threshold_poly terms_eq const_rank coefficient_rank const_closed coefficient_closed
#assert_fields LowerSemicomputableContinuousSemimeasure
  toContinuousSemimeasure approximation approximation_code approximation_computes approximation_nonneg approximation_mono approximation_le approximation_tendsto
#assert_fields MarketComputation
  quote code quote_exact code_spec price_mem_Icc
#assert_fields OccamThresholdEmission
  threshold_sum_codes inverse_width_codes
#assert_fields PGenerableWeighting
  polySeg rank_le closed
#assert_fields PairedWeighting
  polySeg rank_le closed
#assert_fields ParadoxResistanceQuote
  sentence sentence_codes width width_pos width_tendsto_zero diagonal_reflected
  lower_affine upper_affine
#assert_fields ParameterizedDiagonalQuoteCode
  toBooleanQuoteCode body represents_fixedpoint
#assert_fields PaperLUV
  formula unique unit
-- Field-type record (Part I, 2026-08-29).  `structural` changed class: it was
-- `PolyArithmeticFormulaSeq` of the LUVs' Foundation normal forms and is now
-- `PolyArithmeticSourceSeq` of the new `source` field — the paper's own writing of each
-- defining formula, metered one token per *source* node (`def:ec`, tex:753, over the
-- primitive connectives of tex:560).  `compiles` is the bridge: `compile (source n)` is
-- the LUV's Foundation formula, so nothing about the denoted object changed, only what is
-- charged for writing it.  `#assert_fields` freezes names, not types; this note is the
-- freeze on the type.
#assert_fields PaperLUVSeq
  luv source compiles structural
#assert_fields PaperLUVCombination
  luvs termCount const coefficient termCount_poly const_poly coefficient_poly const_rank coefficient_rank const_closed coefficient_closed
#assert_fields PatientSettlementClock
  active active_codes antitone active_through_envelope eventually_inactive settled_of_inactive
-- Metering note (2026-08-27 audit).  Both of these are **whole-value** classes: `code_poly`
-- is `PolyFueled code v`, and `PolyFueled` bundles `IsPolyBounded` of the *output value*
-- alongside the fuel bound, so what is polynomial is the Gödel number, not the symbol
-- count.  `def:ec` meters the time to write an object out (tex:753-755, and explicitly at
-- tex:1931-1933), which admits objects of exponential magnitude, so these are strictly
-- narrower than the paper's class and are charged at each row that takes one rather than
-- once at `def:ec` — see `scripts/coverage-classification.md`'s disclosure section.  The
-- same holds of `PolyRatCodes`, `PolySentenceCodes` and `PolyThresholdCode(Seq)`, and of
-- the structures still carrying them as fields (`PolyPositiveWidths`,
-- `DUSApproximationPresentation`, `DUSThresholdEmission`, `PrefixMachinePresentation`,
-- `PatientSettlementClock`) — which is why several of those rows are `qualified` on a
-- hypothesis invisible in the elaborated signature.
--
-- Correction (2026-08-28 audit, R2-F13/F06).
-- `SemidecidableComputation` (since **retired**, tranche 8), `IntrospectionIntervalQuote`,
-- `SelfTrustQuote` and `ParadoxResistanceQuote` were listed above as whole-value carriers and
-- are **no longer**.  Field by field, as of this commit: `IntrospectionIntervalQuote`
-- carries `BigSentenceCodes` (`source_codes`, `quote_codes`) and `DigitRatCodes`
-- (`inverse_width_codes`); `ParadoxResistanceQuote.sentence_codes` and
-- `SelfTrustQuote.sentence_codes` are `BigSentenceCodes`.  `SelfTrustQuote`'s two remaining
-- threshold fields (`product_codes`, `confidence_codes`) were `LUV.RpnThresholdCodeSeq` —
-- token-metered, not whole-value, and not `PolyThresholdCodeSeq` as the paragraph above
-- implied.  As of 2026-08-31 both are at the write-out `LUV.BigThresholdCodeSeq`; see the
-- migration block below.  The migrated fields are enumerated in the block below.
--
-- ## WRITE-OUT FIELD MIGRATION (2026-08-27/28)
--
-- Every field below moved from a whole-value or token-metered class to a **write-out**
-- class, in which the object's numeric magnitude is unrestricted and only the number of
-- symbols a poly-time writer must emit is bounded.  This is what `def:ec` actually meters
-- (tex:753-755, explicitly at tex:1931-1933).  `#assert_fields` freezes field *names* only,
-- so each type change is recorded here; each is a **widening** of the structure's
-- hypothesis, hence a strengthening of every theorem taking that structure.  In particular
-- `SelfTrustQuote.product_codes` and `.confidence_codes` changed *type* on 2026-08-31, from
-- `LUV.RpnThresholdCodeSeq` to the write-out `LUV.BigThresholdCodeSeq`, and the freeze below
-- passed unchanged — as it always will for a type change.
--
--   `LUV.RpnThresholdCodeSeq` → `LUV.BigThresholdCodeSeq` (2026-08-31):
--     `SelfTrustQuote.product_codes`, `SelfTrustQuote.confidence_codes`.
--
--   `PolySentenceCodes`/`RpnSentenceCodes` → `BigSentenceCodes`:
--     `PolyTradeEmulatable.sentence_poly`, `AffineCombination.PolySequence.sentence_poly`,
--     `RepresentedSemidecidableClaims.sentence_poly` (hence
--     `RepresentedDecidableClaims`), `InconsistentTheoryClaims.inconsistency_poly`
--     (its `.consistency_poly` sibling is **retired**: the consistency family is now the
--     syntactic negation of the inconsistency family, tranche 8),
--     `BitPrefixSentences.prefix_codes`,
--     `CurrentPriceExpectationQuote.sentence_codes`,
--     `IntrospectionIntervalQuote.source_codes` and `.quote_codes`,
--     `ParadoxResistanceQuote.sentence_codes`, `FuturePriceQuote.sentence_codes`,
--     `SelfTrustQuote.sentence_codes`, `EfficientRepeatedEnumeration.sequence_poly`,
--     `FeedbackTraderEmission.sentence_poly`.
--   `PolyNatCodes` → `BigDigits`:
--     `SemidecidableComputation.input_poly` (the structure is since **retired**, tranche 8).
--     CORRECTION (2026-08-30, R7-C1), and its **REPAIR** (2026-08-30, tranche 9-pre): the
--     sentence that stood here — that the premise `hσ : BigDigits (deductionFamilyArg σ)` of
--     `lic_disbelief_inconsistent_theories_unconditional` takes over that role "at the same
--     write-out class" — was **wrong**, and was the one place in this file that oversold a
--     hypothesis.  The retired `input_poly` metered a natural-number *input*, where the
--     base-4 digit count IS the written length, so `BigDigits` there was genuinely the
--     paper's write-out class.  `hσ` applied `BigDigits` to `⌜∼σₙ⌝`, the **Gödel code of a
--     formula**.  Foundation's formula encoding pairs at every node, so the code value is
--     roughly doubly exponential in the parse tree and its digit count roughly `2 ^ depth`
--     — the same failure mode that disqualified `Encodable.encode` as a machine-naming map
--     (see the `DigitMachineCodes` doctrine at `Framework/WriteOut.lean`).  `hσ` was
--     therefore STRICTLY STRONGER than `def:ec` on this lane: it admitted only
--     `O(log n)`-depth (e.g. `binNumeral`-spelled) theory-name families and EXCLUDED
--     paper-admissible families whose source text is short but whose parse tree is deep.
--
--     That premise is **gone**.  The endpoint now takes the day's adjoined axiom by its
--     source text and meters it with `hs : PolyArithmeticSourceSeq s`
--     (`Construction/Witnesses/ArithmeticSource.lean`) — one token per symbol the writer
--     writes, which is `def:ec` verbatim — together with `hcompile`, saying that writing
--     denotes `σₙ`.  What the sentence emits is `ArithSource.sourceNat sₙ`, the run read as
--     a base-`64` numeral with a sentinel (`tokenListNat`, `Framework/CodeSource.lean`),
--     whose base-`4` digit count is `3 * (sourceTokens sₙ).length + 3`: **linear in the
--     written text**, exactly as `Code.sourceNat` is for machines.  The Gödel code is
--     recovered from that numeral *inside* the represented predicate, by
--     `negSourceFormulaCode` (`Construction/Witnesses/SourceNumbering.lean`), which is
--     computable and therefore all `codeOfREPred` consumes — the paper asks only for
--     recursive enumerability there, and the code's size is free.  The class is strictly
--     wider for it: `deepInconsistentSource` is admitted and no digit bound on codes can
--     admit it.  The charge is retired from the `thm:incons` row; the deduction-family
--     paraphrase is the sole remaining one.
--   `RpnSpliceStream` → `BigSpliceStream`:
--     `GeneratedRatFeature.polyTok`.
--
-- MIGRATED (2026-09-02, `thm:scon` widening).  The conditioning lane is no longer a
-- token-metered retention.  `ConditioningPresentation.condition_codes`,
-- `CompactConditioningProcessComputation.condition_codes`, both machine transports
-- (`CondStep.conditionedTranslation_preserves_machine`,
-- `eventualConditionedTranslation_preserves_machine`) and both fuel transports
-- (`RpnConditioning.conditionedTranslation_preserves_ecRpn`,
-- `…eventualConditionedTranslation_preserves_ecRpn`) now take `BigSentenceCodes`.
-- The `_ecRpn` suffix on the two fuel transports is **not** a sentence-class name and was
-- deliberately left unchanged: `ec` names the efficiency class they preserve
-- (`EfficientlyComputable`) and `Rpn` names the RPN *symbol model* their compiler emits
-- in, the sibling lane being `ConditioningCompile.conditionedTranslation_preserves_ecDigit`
-- over the digit model.  Neither theorem mentions any `Rpn` sentence class.
-- `RpnSentenceCodes` survives on this lane only as a convenient sufficient subclass, via
-- `BigSentenceCodes.ofRpnSentenceCodes`.
--
-- What this retires is the **conditioning lane's** token-metered retention, and only that.
-- Token-metered retentions do remain elsewhere on the day-indexed, paper-node-annotated
-- surface, all of them in the LUV *threshold* interfaces
-- (`LUV.RpnThresholdCodes` / `LUV.RpnThresholdCodeSeq`, which unfold to `RpnSentenceCodes`
-- on the threshold family `⌜Xₙ > i/k⌝`, so a census grepping signatures for
-- `RpnSentenceCodes` does not see them):
--   * `LUVCombinationSyntax.threshold_poly` (`Construction/Witnesses/LUVSyntax.lean`), a
--     Tier-2 frozen field, reached by the LI-CANONICAL `_ofSyntax` endpoints — so this one
--     **is** on the canonical endpoint census;
--   * `ConvergencePresentation.threshold_code` (`Properties/ExpectationProperties.lean`);
--   * direct `RpnThresholdCodes` / `RpnThresholdCodeSeq` binders on the `thm:expcoh`,
--     `thm:perexpkno` and `lic_expectation_provind*` endpoints and on the affine tail
--     (`Properties/ExpectationAffine.lean`);
--   * the quote certificates `ExpectedFutureExpectationQuote` (`thm:cee`), `FuturePriceQuote`
--     (`thm:ceu`), `ConditionalExpectationQuote` (`thm:ccee`),
--     `CurrentPriceExpectationQuote` (`thm:epr`) and `CurrentExpectationQuote` (`thm:er`).
-- `LUV.BigThresholdCodeSeq` exists as the write-out counterpart and is what
-- `SelfTrustQuote.product_codes`/`.confidence_codes` were widened to, but the migration of
-- the remaining threshold carriers has not been done.  Why this is a *rendering
-- sensitivity* rather than a narrowing of the paper's admissible LUVs — the threshold
-- route meters a formula string over a fixed finite alphabet (`0..19`), so the per-token value
-- clause is vacuous along it — is worked out in
-- `scripts/coverage-classification.md`, *LUV-threshold metering: rendering sensitivity,
-- witnessed*.
--
-- The obstruction this file previously recorded here was **mis-diagnosed**, and the record
-- is corrected rather than merely updated.  It claimed that `machineSentenceBlocks_of_rpn`
-- clocked the certificate in a way only a value-bounded stream supports, so that widening
-- meant a `BigSentenceCodes → CondStep.MachineSentenceBlocks` re-blocking in `FP` at the
-- scale of `CondStep.lean`'s own `_mem_FP` suite.  Both halves were wrong.  (a) The digit
-- clamp `min · 4` is the identity because the clamped object is literally a list of base-4
-- digits and terminators — `CondStep.mem_digitize_le_four` is a fact about `digitize ts`
-- for an ARBITRARY token list `ts`, and bounds no token's value.  (b) A write-out stream
-- does supply the clock: `PolySegStream.undigitizeTokens` reads a poly-fueled token count
-- and `BigDigits` per-token digit access off the certificate's own digit stream, and
-- `BigDigits.blockSeg |>.concatVar` re-emits the canonical digitization.  Packaged as
-- `BigTokenStream.digitizeStream` (`Framework/WriteOut.lean`, ~12 lines), it makes
-- `machineSentenceBlocks_of_big` a hypothesis-type change with no proof-body edit, and
-- every downstream consumer widens the same way.  No `_mem_FP` lemma was added.
--
-- MIGRATED (2026-08-31, FINAL-audit defect 4).  `lic_self_trust_closed` (`thm:st`) no longer
-- sits at `RpnSentenceCodes φ`; it takes `hφ : BigSentenceCodes φ`, like every other closed
-- endpoint.  The write-out threshold class `LUV.BigThresholdCodeSeq`
-- (`Framework/Expectations.lean`) now **exists** — `BigSentenceCodes` at the same
-- `⟨n,⟨k,i⟩⟩` paired index `LUV.RpnThresholdCodeSeq` uses — with
-- `LUV.RpnThresholdCodeSeq.toBig` the embedding and `LUV.BigThresholdCodeSeq.reindex` the
-- reindexing.  `SelfTrustQuote.product_codes` and `.confidence_codes` are widened to it,
-- `indicatorProductLUV_rpnThresholdCodeSeq` is now `indicatorProductLUV_bigThresholdCodeSeq`
-- (`BigSentenceCodes.and` supplies the `⋏`-shell token), and `paperConfidenceQuoteCode`
-- takes `BigSentenceCodes` — it consumed its hypothesis only through `.primrec`.  Nothing on
-- the self-trust lane opened a threshold certificate as value-bounded emission data: every
-- consumer either reindexes it (`.comp`/`.reindex`) or hands it to
-- `AffineCombination.PolySequence`, whose `sentence_poly` field is already write-out metered
-- — which is why this was a widening at each binder, not a rebuild of the splice.
--
-- Widened in this change (2026-08-28 audit, R2-F11), each having consumed its sentence-codes
-- hypothesis only through `.primrec`, which `BigSentenceCodes.primrec` supplies:
-- `paperPriceQuoteCode` and `lic_expectations_of_probabilities_closed` (`thm:epr`),
-- `paperFutureQuoteCode` and `lic_no_expected_net_update_closed` (`thm:ceu`),
-- `paperIntervalQuoteCode` and `lic_introspection_closed` (`thm:ref`).  Those three closed
-- paper endpoints now admit sentence families whose Gödel codes are exponential while their
-- emitted symbol count stays polynomial.
-- Retired from the Tier-2 freeze (2026-08-28 audit, R2-F15/F18).  `PolyMachineCodes` and
-- `PolyNatCodes` were inventoried under a `Paper node: def:ec` line they did not earn: both
-- bound the *numeric value* of a name, which is precisely what `def:ec`'s write-out metering
-- does not bound.  They are now what they always were — strictness foils, named only inside
-- `not_polyNatCodes_ack`, `bigDigits_two_pow_not_polyNatCodes` and
-- `digitMachineCodes_nest_not_polyMachineCodes` — so they carry no paper annotation and are
-- not trust surface.  The paper's machine-naming class, `DigitMachineCodes`, carries the
-- `def:ec` line in their place.
--
-- Accounting correction (2026-08-28 audit, R3-F07/R3-F08).  `PolyNatCodes` is named in one
-- place beyond those foils: it is a *hypothesis* of `quotationClaimSentence_poly`
-- (`Construction/Witnesses/QuotationAffine.lean:67`), which is the one remaining internal
-- helper taking it.  (`semanticPrimeSentence_poly` was the second; it had no callers and was
-- deleted in the same change.)  That hypothesis bounds a **caller-chosen index sequence**,
-- never the paper's `⟨x⟩`, so it levies no charge on a paper-facing statement — but the
-- retirement note above should not be read as saying the class occurs nowhere else.
-- Framework/CodeSource.lean, Framework/WriteOut.lean — the machine-naming map that
-- `DigitMachineCodes` is built on (2026-08-28 audit, R3-F24).  `DigitMachineCodes` carries
-- the `Paper node: def:ec` line for machine names, and it is worth exactly what `sourceNat`
-- and `ofSource` are worth: the linearity bound `len4_sourceNat_le` (`len4 c.sourceNat ≤
-- 2 * c.size`) is what makes the name writable in time polynomial in the day, and the
-- decoder is what makes the name a name rather than a hash.  Those guarantees were
-- axiom-checked only by `#print axioms` inside their own file, with no block here.
--
-- The decoder's cost is now stated, not assumed (R3-F02/F06/F13).  `ofSource` previously
-- peeled one digit per unit of the name's *value* — primitive recursive and correct, and
-- 18158869 peel steps on a 7-node code — while the docstrings called it "efficiently
-- decodable".  It now peels `len4 n` digits: `ofSource_peelSteps` gives the exact step
-- count and `sourceNat_peelSteps_le` bounds it by `2 * c.size`.  `size_le_len4_sourceNat`
-- is the fuel-adequacy side condition that makes the roundtrip go through, and
-- `len4_primrec` (Framework/DigitArith.lean) is what keeps `ofSource` primitive recursive
-- once its fuel is a digit count.  No `PolyFueled`/`Complexity.FP` certificate is claimed
-- for `ofSource`, and none is inventoried here.
--
-- Only `DigitMachineCodes` is listed: the inventory contract is fail-closed both ways —
-- `scripts/check-paper-nodes.sh` requires every inventoried member to carry a `Paper node`
-- annotation — and the supporting declarations are internal, so annotating them to make
-- them listable would be exactly the over-broad labelling this same audit trimmed
-- elsewhere.  They remain axiom-checked by the `#print axioms` block at the foot of
-- `Framework/CodeSource.lean`, which covers, in that file, `sourceNat`,
-- `pow_pred_le_sourceNat`, `len4_sourceNat_le`, `size_le_len4_sourceNat`, `ofSource`,
-- `ofSource_peelSteps`, `sourceNat_peelSteps_le`, `ofSource_sourceNat` and
-- `ofSource_primrec`, and by the block in `Framework/DigitArith.lean` for `len4_primrec`.
-- A future change that widens the inventory contract should pull them in here.
#assert_axioms_clean
  DigitMachineCodes

#assert_fields PrefixMachinePresentation
  sentence sentence_codes approximation approximation_nonneg approximation_le
  approximation_tendsto kraft covers
#assert_fields PrefixNegationCompiler
  overhead complexity_neg_le
-- FIELD REMOVAL (tranche 7).  `QuotationTheoryPresentation` no longer carries
-- `theory_sigmaOne : 𝗜𝚺₁ ⪯ T`.  This is a loud Tier-2 freeze change: the field is gone from
-- the block below, and every inhabitant (`quotationPresentation`,
-- `ProductDefinition`'s stage-extension transport) drops the corresponding
-- `theory_sigmaOne := …` line.  The field was never a hypothesis of the quotation
-- presentation's own content — its only two consumers were on the `thm:lp` diagonal path,
-- `ParameterizedDiagonalQuoteCode.diagonal_law` and `paradoxResistanceQuoteOfDiagonal`,
-- each of which opened it with `letI : 𝗜𝚺₁ ⪯ T := Q.theory_sigmaOne` in order to reach
-- Foundation's `parameterized_diagonal₁`.  Those two now take an ordinary `[𝗜𝚺₁ ⪯ T]`
-- instance binder, so `thm:lp` still charges `𝗜𝚺₁` (legitimately, at the one step that
-- spends it) while the seven closed quotation endpoints, which merely *inherited* the field,
-- no longer charge it at all.  `diagonal_law` additionally lost its `(Q : …)` and `{DP}`
-- arguments, which became unused once the `letI` was gone; it has no callers in the library.
#assert_fields QuotationTheoryPresentation
  toComputationTheoryPresentation quote_positive_enters quote_negative_refutes
#assert_fields RationalQuoteCode
  code value_mem pos_complete neg_complete threshold_poly
#assert_fields RepresentedDecidableClaims
  toRepresentedSemidecidableClaims disprovable_of_false
#assert_fields RepresentedSemidecidableClaims
  sentence sentence_poly provable_of_true
#assert_fields SelfTrustQuote
  delta_pos probability_mem sentence_codes probability_generable product_codes
  confidence_codes confidence_reflected product_reflected affine
#assert_fields SettlementChecker
  code spec
#assert_fields Strategy
  trades rank_le
#assert_fields StrictSeparatorPresentation
  constraint repetition jointly_possible consistentAt class_covers mass_class_tendsto_zero
#assert_fields Trader
  strat
#assert_fields UniversalContinuousSemimeasure
  toLowerSemicomputableContinuousSemimeasure universal


end LogicalInduction

/-! ## ModalAgents — modal open-source game theory (Barász et al.)

Every ModalAgents endpoint is now strictly clean. The former sole intentional axiom
`glFixedPoint_thm42` (GL fixed-point existence) is discharged by the `ProvabilityLogic/`
development (vendored from FormalizedFormalLogic/ProvabilityLogic, pinned in
`lakefile.lean`; see `ModalAgents/FixedPoint.lean`); `glFixedPoint_thm42`
is a proved theorem, so the cooperation endpoints that rest on it are asserted strictly
clean below rather than via `#assert_axioms_clean_except`.

That paper numbers its nodes off a single section-scoped counter shared by
`theorem`/`lemma`/`proposition`/`corollary`/`condition`, and only 22 of them carry a
LaTeX `\label`, so — as for Cartesian Frames — the printed `Theorem 4.7` style number is
the provenance key rather than a label. `Paper node:` lines on the endpoints below cite
those numbers, and `scripts/check-modal-agents-nodes.py` validates them against the
committed TeX (`ModalAgents/notes/1401.5577-main.tex`) **and** checks that every
*declaration* annotated in `ModalAgents/` is itself listed between the MA-INVENTORY
markers below.

Several listed endpoints carry no annotation of their own, because they render no
numbered node of that paper. They are all `lemma`s or definitions, per the repo's keyword
rule, and they stay inventoried and axiom-checked regardless:

* `subst_congr` — a GL-level substitution congruence; the paper's Lemma 4.5 is the
  *arithmetic* statement, carried by `arithmetic_modal_substitution`.
* `glFixedPoint_uniqueness` — the *rule* form of Theorem 4.3, derived from the printed
  internal form `glFixedPoint_uniqueness_internal` (which carries the annotation) by
  necessitation; it is the form the modal-agent development consumes.
* `arithInterp` and `Realization.update` — the definitions the arithmetic statements are
  phrased in: `arithInterp f φ` is the paper's `φ(ψ₁,…,ψₙ)`, and `Realization.update`
  substitutes for the diagonal variable. Listed because they are statement surface.
* The §4 arithmetic-agent vocabulary — `Agent`, `Agent.app`, `opponentRealization`,
  `IsModalAgentOfRank`, `IsModalAgent`, `BehaviorallyEquivalent`, `IsBehavioral`,
  `cliqueBotSpec`, `cliqueBot`, `cliqueBotVariant`. These are the paper's §4 and §2
  definitions ("agent", "`[X(Y)]`", "modal agent of rank `k`", "behaviorally
  equivalent", "behavioral agent", CliqueBot). That paper's `definition` environment is
  an uncounted `trivlist`, so none of them *can* cite a node; they are listed because
  they are the statement surface of `modalAgent_isBehavioral` and
  `cliqueBot_not_modalAgent`, and reading either endpoint means reading them.
* `cooperateBot_isModalAgentOfRank_zero` — the non-vacuity witness for
  `IsModalAgentOfRank`: CooperateBot (action formula `⊤`) is a modal agent of rank 0, so
  Theorem 4.8 is not a statement about an empty class and Corollary 4.9 separates
  CliqueBot from a class that has members. The paper introduces CooperateBot in §2 and
  never numbers this.
* The Corollary 4.9 proof steps — `cliqueBot_app` (CliqueBot cooperates exactly with
  agents carrying its own code, the quining that makes it CliqueBot at all),
  `cliqueBotVariant_ne`, `cliqueBot_behaviorallyEquivalent_variant`,
  `cliqueBot_cooperates_self`, `cliqueBot_defects_variant` and
  `cliqueBot_not_isBehavioral`. These are the clauses of that corollary's one-sentence
  printed proof, not numbered nodes. They are listed rather than left internal because
  the corollary is a *negative* result: what makes it non-trivial is that `cliqueBot`
  really is CliqueBot and the variant really is behaviorally equivalent to it, and those
  are exactly the facts above.
* `defectBot_defects`, `defectBot_provably_defects` and `cooperateBot_cooperates` —
  the §2 remark that `PA ⊢ [CB(X)=C]` and `PA ⊢ [DB(X)=D]`, prose in an unnumbered
  `remark`.
* `fairBot_unexploitable`, `fairBot_vs_cooperateBot` and `fairBot_vs_defectBot` — §3
  prose on FairBot's unexploitability ("by inspection") and its waste against
  CooperateBot, again unnumbered.
* `prudentBot_vs_defectBot` — the "in particular, PA+1 ⊢ [PB(DB)=D]" step *inside* the
  proof of Theorem 3.2, not one of that theorem's four conjuncts.
* The defection-boundary block — `ProvablyDefects.defects`, the three outcome
  reductions `outcome_fairBot_defectBot`, `outcome_prudentBot_defectBot`,
  `outcome_prudentBot_cooperateBot`, and the three negative results
  `fairBot_not_provably_defects_defectBot`,
  `prudentBot_not_provably_defects_defectBot`,
  `prudentBot_not_provably_defects_cooperateBot`. These are *this development's* own
  accounting rather than paper nodes: they pin down exactly how far `Defects` (which
  is `GL ⊬ outcome`, weaker than the paper's provable defection) can be strengthened
  to `ProvablyDefects` (`GL ⊢ ∼outcome`, the paper's notion). The answer is: on
  DefectBot's side, all the way; on the other three endpoints, not at all, because
  their outcome formulas are GL-equivalent to `□⊥`, `□⊥` and `□□⊥`, so provable
  defection would require `GL` to prove `Con(PA)` or `Con(PA+1)`. That is exactly why
  the paper states those three in `PA+1`/`PA+2`. They are listed here so a regression
  in the obstruction argument fails the build alongside the endpoints it excuses. -/

-- MA-INVENTORY-BEGIN
#assert_axioms_clean
  subst_congr glFixedPoint_uniqueness glFixedPoint_uniqueness_internal glFixedPoint_thm42
  glFixedPoint_spec outcome_fixed_point
  lob_theorem arithInterp Realization.update
  arithmetic_modal_substitution arithmetic_fixedPoint_uniqueness
  Agent Agent.app opponentRealization IsModalAgentOfRank IsModalAgent
  cooperateBot_isModalAgentOfRank_zero
  BehaviorallyEquivalent IsBehavioral modalAgent_isBehavioral
  cliqueBotSpec cliqueBot cliqueBotVariant
  cliqueBot_app cliqueBotVariant_ne cliqueBot_behaviorallyEquivalent_variant
  cliqueBot_cooperates_self cliqueBot_defects_variant
  cliqueBot_not_isBehavioral cliqueBot_not_modalAgent
  defectBot_defects defectBot_provably_defects ProvablyDefects.defects
  cooperateBot_cooperates
  fairBot_vs_fairBot fairBot_unexploitable fairBot_vs_cooperateBot
  rank0_fairBot_implies_cooperateBot
  fairBot_vs_defectBot prudentBot_vs_fairBot prudentBot_vs_defectBot
  prudentBot_vs_cooperateBot prudentBot_vs_prudentBot prudentBot_unexploitable
  outcome_fairBot_defectBot outcome_prudentBot_defectBot
  outcome_prudentBot_cooperateBot
  fairBot_not_provably_defects_defectBot
  prudentBot_not_provably_defects_defectBot
  prudentBot_not_provably_defects_cooperateBot
  Cooperates.arithmeticLift ProvablyDefects.arithmeticLift modalAgent_behavioral
-- MA-INVENTORY-END

/-! ## Concrete arithmetic instantiation

Everything above is asserted of the endpoints **as stated**, and the arithmetic-quotation
family (`thm:cee`, `thm:ceu`, `thm:ccee`, `thm:st`, `thm:ref`, `thm:epr`, `thm:er`,
`thm:lp`, `thm:halts`, …) is stated parametrically over an arithmetic theory:
`(T : ArithmeticTheory) [T.Δ₁] [Entailment.Consistent T]` plus, per lane, `[𝗣𝗔⁻ ⪯ T]` or
`[𝗜𝚺₁ ⪯ T]` — the consistency binder having replaced `[T.SoundOnHierarchy 𝚺 1]` on
2026-08-30, when the quotation schemas became value fibers of one `code` formula, and the
`𝗜𝚺₁` binder having been *deleted* in tranche 7 everywhere it was unused.

**The census, and how it is taken.** Both figures below are measured by elaborating a
generated file of `#check @name`, one line per name in the `LI-CANONICAL-BEGIN` …
`LI-CANONICAL-END` block above, and grepping the *printed* binder lists — never by reading
docstrings, and never by grepping the sources, which is how the `[ISigma 1 ⪯ T]` spelling in
the semantic-lifted lane stayed invisible for two tranches.

  * `[T.SoundOnHierarchy 𝚺 1]` — **0 of 105**. Down from 16, in three migrations; the last
    (2026-08-30) removed twelve at once, all of which reached the instance through
    `theoremDP_hworld`'s tag 7. The paper treats soundness as a further assumption it
    explicitly declines (tex:2673), and nothing here takes it. The only surviving occurrence
    of the name anywhere in `LogicalInduction/` is `loopsTheory_soundOnSigma1`, a fact about
    one concrete theory used as a non-vacuity witness for `thm:loops`'s `hloops`.
  * `𝗣𝗔⁻ ⪯ ·` — **16 of 105**, and `𝗥₀ ⪯ ·` — **0**.  `thm:incons` carried the last one
    redundantly, beside the stronger `𝗣𝗔⁻` it also carries; it was dropped on 2026-08-30
    and the binder is gone from the elaborated signature, Foundation's
    `instance [𝗣𝗔⁻ ⪯ T] : 𝗥₀ ⪯ T` (`Arithmetic/Schemata.lean`) supplying it.
    `T.Δ₁` — **23 of 105**.  Note that
    `𝗣𝗔⁻` is **not** implied by "Θ represents computations", though an earlier edition of the
    classification ledger said it was: the paper's premise gives `Θ ⊬ n̄ = m̄` for `n ≠ m` but
    never `Θ ⊢ n̄ ≠ m̄`, and Robinson's R represents every computable function without
    containing `𝗣𝗔⁻`.  It is a genuine, small strengthening, spent on the compact-`binNumeral`
    value transfer that `def:ec` forces and on `code_uniq`'s `rfind` case — the object-level
    fiber exclusivity that replaced Σ₁-soundness at tag 7.  Disclosed globally in
    `scripts/coverage-classification.md`; its charging (global vs per row) is pending a ruling.
  * `𝗜𝚺₁ ⪯ ·` (either spelling) — **3 of 105**, in each case because a proof step spends it,
    and in each case the substrate's own indexing rather than a theory-strength assumption
    the statement needs: `unitFracPaperLUVSeq` and `unitFracPaperLUVBoundedSequence`, the two
    literal-`PaperLUV` frontends, whose `threshold_provable_of_neg` / `rationalCutAt` /
    `source_valued` steps prove rational-cut arithmetic *inside* `T`; and
    `lic_paradox_resistance_ofDiagonal_unconditional` (`thm:lp`), whose diagonal is
    Foundation's `parameterized_diagonal₁`, stated over `𝗜𝚺₁`.  That endpoint prints
    `[T.Δ₁] [Entailment.Consistent T] [𝗜𝚺₁ ⪯ T]` and carries **no** `[𝗣𝗔⁻ ⪯ T]`: the two
    would be redundant (`𝗜𝚺₁ ⪯ T` implies `𝗣𝗔⁻ ⪯ T` by instance), so that endpoint is
    declared *outside* the `𝗣𝗔⁻` section of `ComputationDP.lean` and recovers the weaker
    instance in its proof term, where `paperLIA`/`theoremDP_hworld` need it.  `omit`
    cannot do this job: it does not take the variable out of the local context, so instance
    search still reaches it from the conclusion's `paperDiagonalQuoteCode`.  It is therefore
    not one of the 17 above.

The tranche-7/D step that closed the last eight was deleting `theory_sigmaOne` from
`QuotationTheoryPresentation` (see the FIELD REMOVAL note above): the seven closed quotation
endpoints (`thm:ref`, `thm:st`, `thm:epr`, `thm:er`, `thm:cee`, `thm:ceu`, `thm:ccee`)
inherited `𝗜𝚺₁` from that field and from no step of their own, and now all seven read
`[T.Δ₁] [𝗣𝗔⁻ ⪯ T] [Entailment.Consistent T]`.  `thm:ccee` additionally required migrating the
semantic-lifted lane (`SemanticQuote`, `SemanticQuoteFactor`, `OldLanguageLift`,
`SemanticRegistryProduct`, `SemanticLiftedCCEE`), where the same binder was spelled
`[ISigma 1 ⪯ T]` rather than `[𝗜𝚺₁ ⪯ T]` and so was invisible to the earlier tranches' greps;
all 64 of those sites are now `[𝗣𝗔⁻ ⪯ T]`.  Those endpoints are axiom-clean, but only because
the theory data are *hypotheses*.

Instantiating them at a concrete theory is a different claim, and it is pinned here so that
a regression would fail the build. At the pinned Foundation revision it costs nothing:
`Δ₁`-definability of `𝗜𝚺₁` and `𝗣𝗔` is *proved* — `ISigma1_delta1Definable` and
`PA_delta1Definable` are instances discharged in
`Foundation/FirstOrder/Incompleteness/InductionSchemeDelta1.lean`, which replaced the two
`axiom`s that formerly sat in `Examples.lean`. The instantiation below is therefore
asserted under ordinary `#assert_axioms_clean`. -/

open LO LO.FirstOrder LO.FirstOrder.Arithmetic in
/-- `thm:ceu` at the concrete theory `𝗜𝚺₁`. -/
noncomputable def concreteArithmeticInstantiation :=
  @LogicalInduction.lic_no_expected_net_update_closed 𝗜𝚺₁ inferInstance inferInstance
    inferInstance

#assert_axioms_clean concreteArithmeticInstantiation

/-! ### No Σ₁-soundness is asked for at a concrete theory (2026-08-30)

`thm:ref` elaborates exactly three instance arguments — `[T.Δ₁]`, `[𝗣𝗔⁻ ⪯ T]` and
`[Entailment.Consistent T]` — and `thm:lp` exactly three as well: `[T.Δ₁]`,
`[Entailment.Consistent T]`, and the `[𝗜𝚺₁ ⪯ T]` its diagonal genuinely spends, with no
`[𝗣𝗔⁻ ⪯ T]` beside it.  Both would fail to typecheck as written if
`[T.SoundOnHierarchy 𝚺 1]` were still in either binder list; the arity is also the live
regression test for tranche 7's `𝗜𝚺₁` deletion, since restoring the binder on `thm:ref` would
give it a fourth argument.  The corresponding `grep` is
`grep -rn SoundOnHierarchy LogicalInduction/ | grep -v loopsTheory`, which now finds prose
only. -/

open LO LO.FirstOrder LO.FirstOrder.Arithmetic in
/-- `thm:ref` at the concrete theory `𝗜𝚺₁`, soundness-free. -/
example := @LogicalInduction.lic_introspection_closed 𝗜𝚺₁ inferInstance inferInstance inferInstance

open LO LO.FirstOrder LO.FirstOrder.Arithmetic in
/-- `thm:lp` at the concrete theory `𝗜𝚺₁`, soundness-free. -/
example :=
  @LogicalInduction.lic_paradox_resistance_ofDiagonal_unconditional 𝗜𝚺₁
    inferInstance inferInstance inferInstance

/-! ### `thm:ref` below `𝗜𝚺₁` (tranche 7/D)

The two examples below are the positive witness that tranche 7/D's deletion of
`QuotationTheoryPresentation.theory_sigmaOne` actually widened the closed quotation lane, not
merely renamed a binder.  `lic_introspection_closed` now instantiates at `𝗣𝗔⁻` itself —
a theory that proves **no** induction, so `𝗜𝚺₁ ⪯ 𝗣𝗔⁻` is false and no `𝗜𝚺₁` instance is
available anywhere in the elaboration.  Before the field was removed this did not typecheck.
The `𝗣𝗔` instantiation is the same statement at the theory the paper actually cares about. -/

open LO LO.FirstOrder LO.FirstOrder.Arithmetic in
/-- `thm:ref` at `𝗣𝗔⁻`, with no `𝗜𝚺₁ ⪯ ·` instance in scope. -/
example :=
  @LogicalInduction.lic_introspection_closed 𝗣𝗔⁻ inferInstance inferInstance inferInstance

open LO LO.FirstOrder LO.FirstOrder.Arithmetic in
/-- `thm:ref` at the concrete theory `𝗣𝗔`. -/
example :=
  @LogicalInduction.lic_introspection_closed 𝗣𝗔 inferInstance inferInstance inferInstance

/-! ## Cartesian Frames — endpoint inventory

Same contract as the Logical Induction inventory above, for `CartesianFrames/`
(paper: arXiv:2109.10996). Most of that paper's nodes carry no LaTeX `\label`, so
`Paper node:` lines cite the printed `Definition n` / `Claim n` / `Theorem n`
numbers; `scripts/check-cartesian-frames-nodes.py` validates them against the
committed TeX **and** checks that every *declaration* annotated in the library is
itself listed between the CF-INVENTORY markers below — sharing a node with a listed
declaration is not enough. Five groups of listed names carry no annotation of their own:
the constructive carriers of Appendix B's Claims 46 and 48 (`Frame.dualEquivalence`,
`Frame.zeroIsInitial`, `Frame.topIsTerminal` — the `theorem`s state the paper's
propositional content, these are the data behind them); the four unnumbered facts the
paper uses silently (`Frame.Biextensional.nonempty_iso_collapse`, the step taken
whenever a biextensional frame is replaced by its collapse, together with the three
`≃ᵇ`-invariants `Frame.image_eq_of_biextEquiv`,
`Frame.exists_env_injective_of_biextEquiv` — the standard refuters for `◁ₓ` and `◁₊` —
and `Frame.BiextEquiv.dual`, which every dualized definition runs on); the
inhabitation of Definition 31's choice functions (`Frame.partitionSectionsOut` and the
`Nonempty` instance built from it, which the paper assumes without comment); the two
combined-iff convenience wrappers (`Frame.addSubagent_iff_addSubagentCategorical`,
whose two halves are the annotated Claims 55 and 56, and its multiplicative sibling
`Frame.multSubagent_iff_multSubagentCategorical`, the composite of Claims 59 and 60); and the last three blocks, the
non-vacuity, subagency, and operation/Appendix-B witnesses of
`CartesianFrames/Examples.lean`, listed here so that the separations they assert are
axiom-checked alongside the definitions they constrain. -/

open CartesianFrames in
-- CF-INVENTORY-BEGIN
#assert_axioms_clean
  Frame Frame.image Frame.Hom Frame.Hom.comp Frame.instChuCategory
  Frame.dual Frame.Hom.dual Frame.dualFunctor
  Frame.Hom.IsIsomorphism Frame.nonempty_iso_iff_exists_isIsomorphism
  Frame.Biextensional
  Frame.agentSetoid Frame.envSetoid Frame.collapse Frame.BiextEquiv
  Frame.Homotopic Frame.HomotopyEquiv
  Frame.Biextensional.nonempty_iso_collapse
  Frame.nonempty_iso_of_eq Frame.biextEquiv_of_nonempty_iso
  Frame.homotopyEquiv_iff_nonempty_iso_of_biextensional
  Frame.biextEquiv_iff_homotopyEquiv
  Frame.image_eq_of_biextEquiv Frame.exists_env_injective_of_biextEquiv
  Frame.BiextEquiv.dual
  Frame.mapWorlds Frame.BiextEquiv.mapWorlds Frame.curry
  Frame.botOf Frame.instBot Frame.botOfUnivIsoBot Frame.homBotEquiv
  Frame.Subagent Frame.SubagentCurry Frame.SubagentCovering
  Frame.subagent_iff_subagentCovering
  Frame.SubagentCovering.subagentCurry Frame.SubagentCurry.subagent
  Frame.subagent_iff_subagentCurry
  Frame.Subagent.trans Frame.Subagent.of_biextEquiv Frame.Subagent.refl
  Frame.AddSubagent Frame.MultSubagent
  Frame.AddSubagentCurry Frame.MultSubagentCurry
  Frame.AddSubagent.addSubagentCurry Frame.AddSubagentCurry.addSubagent
  Frame.MultSubagent.multSubagentCurry Frame.MultSubagentCurry.multSubagent
  Frame.addSubagent_iff_addSubagentCurry Frame.multSubagent_iff_multSubagentCurry
  Frame.AddSubagent.subagent Frame.MultSubagent.subagent
  Frame.AddSubagent.congr Frame.MultSubagent.congr
  Frame.AddSubagent.refl Frame.MultSubagent.refl
  Frame.AddSubagent.trans Frame.MultSubagent.trans
  Frame.subagent_iff_exists_multSubagent_addSubagent
  Frame.SubEnv Frame.AddSubEnv Frame.MultSubEnv
  Frame.multSubagent_iff_multSubEnv
  Frame.commit Frame.commitCompl Frame.assume Frame.assumeCompl
  Frame.commit_addSubagent Frame.commitCompl_addSubagent
  Frame.addSubEnv_assume Frame.addSubEnv_assumeCompl
  Frame.partitionSections
  Frame.partitionSectionsOut Frame.instNonemptyPartitionSections
  Frame.external Frame.externalQuot Frame.internal Frame.internalSect
  Frame.external_multSubagent Frame.externalQuot_multSubagent
  Frame.multSubagent_internal Frame.multSubagent_internalSect
  Frame.commit_commit_self Frame.commitCompl_commitCompl_self
  Frame.assume_assume_self Frame.assumeCompl_assumeCompl_self
  Frame.dualEquivalence Frame.dualFunctor_isEquivalence
  Frame.dualEquivalence_functor_comp_inverse Frame.dualEquivalence_inverse_comp_functor
  Frame.instZero Frame.instTop
  Frame.zeroIsInitial Frame.topIsTerminal
  Frame.nonempty_isInitial_zero Frame.nonempty_isTerminal_top
  Frame.oneOf Frame.instOne Frame.oneOfUnivIsoOne
  Frame.AddSubagentCategorical Frame.MultSubagentCategorical
  Frame.AddSubagentCategorical.addSubagent Frame.AddSubagent.addSubagentCategorical
  Frame.addSubagent_iff_addSubagentCategorical
  Frame.multSubagent_iff_multSubagentCategorical
  Frame.MultSubagentSubEnv
  Frame.multSubagentCategorical_iff_multSubagentSubEnv
  Frame.multSubagentSubEnv_iff_multSubagent
  -- Non-vacuity witnesses (CartesianFrames/Examples.lean).
  Examples.driver_biextensional
  Examples.seven_mem_driver_image Examples.two_not_mem_driver_image
  Examples.dedup_biextensional Examples.not_dup_biextensional
  Examples.homotopyEquiv_dedup_dup Examples.not_nonempty_iso_dedup_dup
  Examples.homotopyEquiv_strictly_weaker_than_iso
  Examples.biextEquiv_strictly_weaker_than_iso
  Examples.homotopic_ne_eq Examples.not_homotopic_of_row_col
  Examples.not_nonempty_hom_dedup_driver Examples.not_homotopyEquiv_dedup_driver
  Examples.not_biextEquiv_dedup_driver
  Examples.nonempty_iso_dup_collapse_dedup
  Examples.not_nonempty_iso_dup_collapse
  -- Subagency witnesses (CartesianFrames/Examples.lean).
  Examples.not_subagent_dedup_driver
  Examples.driver3_biextensional Examples.driver_addSubagent_driver3
  Examples.not_biextEquiv_driver_driver3
  Examples.teamZ_image_univ Examples.teamC_multSubagent_teamD
  Examples.teamC_biextensional Examples.teamD_biextensional
  Examples.not_biextEquiv_teamC_teamD
  Examples.not_subagent_driver3_driver Examples.not_subagent_teamD_teamC
  Examples.bigC_biextensional Examples.bigC_subagent_bigD
  Examples.not_bigC_multSubagent_bigD Examples.not_bigC_addSubagent_bigD
  Examples.every_witness_nontrivial Examples.bigC_decomposes
  -- Operation and Appendix-B witnesses (CartesianFrames/Examples.lean).
  Examples.externalBigD_multSubagent_bigD Examples.bigD_biextensional
  Examples.bigD_outcome_inj Examples.bigDCells_ne
  Examples.externalBigD_biextensional Examples.not_biextEquiv_externalBigD_bigD
  Examples.externalBigD_multSubagent_not_biextEquiv
  Examples.not_biextEquiv_driver3_driver3Assume
  Examples.colDupLoop_homotopy_factors Examples.colDup_addSubagentCategorical_self
  Examples.colDupLoop_no_exact_factorization Examples.colDup_two_distinct_endos
  Examples.colDup_addSubagentCategorical_oneCol
  Examples.not_exact_factorization_colDup_oneCol
-- CF-INVENTORY-END

/-! Tier-2 boundary structures for the Cartesian Frames surface (same contract as
the Logical Induction `#assert_fields` block). -/
#assert_fields CartesianFrames.Frame
  Agent Env outcome
#assert_fields CartesianFrames.Frame.Hom
  agent env adjoint
#assert_fields CartesianFrames.Frame.Biextensional
  agent_ext env_ext

/-! ## Finite Factored Sets — the checked endpoint inventory

Same contract as the CF-INVENTORY block above: every declaration carrying a
`Paper node:` annotation in `FiniteFactoredSets/` must itself be listed between the
FFS-INVENTORY markers below, and `scripts/check-finite-factored-sets-nodes.py` enforces
that direction, together with the validity of each cited node against the committed TeX and
the anchoring of each annotation to a named declaration.

Read that as the one direction it is.  The checker does **not** enforce the converse — that
every name listed below is a real, annotated declaration — and could not: this block also
carries the non-vacuity witnesses, so it holds several times as many entries as there are
annotations.  A line naming a declaration that does not exist passes the Python checker and
is caught only when this file is elaborated, by `#assert_axioms_clean` failing to resolve
the name.  `lake build AxiomAudit` is part of the contract, not an independent check of it.
Nor does anything mechanically check that the paper's in-scope nodes are all covered; that
accounting is prose in `FiniteFactoredSets/README.md`, to be re-derived by hand (compare
`grep -rho "Paper node: [A-Za-z]* [0-9]*" FiniteFactoredSets/*.lean | sort -u` against
`scripts/paper_nodes.py`'s `printed_independent_declarations`).

This formalization is **complete** for its ruled scope: the list below covers §2–§7 —
every in-scope node has a carrier or is Mathlib-rendered; Conjecture 1 (§7.2) is listed as
a stated `Prop` that nothing proves, and Example 3 is out of scope by ruling (Example 4 was
brought into scope 2026-08-30 and is carried by the `InfiniteExamples` entries below).  Nine of
the paper's nodes have no Lean carrier at all because they are rendered by
Mathlib vocabulary under the `dd:` tags in `FiniteFactoredSets.lean`.  Six are in §2.1 —
Definition 1 (the disjoint union `⊔S`) is absorbed into `Setoid` and the dependent product,
Definition 2 (partition) is `Setoid`, Definition 5 (`∼_X`) is the setoid relation,
Definition 6 (finer) is `≤`, Definition 7 (`Dis_S`/`Ind_S`) is `⊥`/`⊤`, and Definition 9
(`∏(B)`) is the dependent product — and three are outside it: §5.1's Definitions 29
(evaluation) and 30 (support) and §6.1's Definition 39 (preimages).  Nine plus the 88
carried below is the 97 in-scope nodes.  Those nine are recorded in
`FiniteFactoredSets/README.md` rather than
inventoried here, because there is no declaration of this project's to axiom-check. -/

open FiniteFactoredSets in
-- FFS-INVENTORY-BEGIN
#assert_axioms_clean
  part equivalence_setoid IsTrivialPartition bot_le_and_le_top commonRefinement
  IsFactorization FactoredSet FactoredSet.eq_of_forall_rel
  isFactorization_iff_existsUnique FactoredSet.eq_of_part_eq
  FactoredSet.chimeraFun FactoredSet.chimera FactoredSet.chimeraImage
  FactoredSet.chimera_spec
  IsTrivialFactorization existsUnique_trivialFactorization
  FactoredSet.size FactoredSet.dim FactoredSet.finite_basis_of_finite
  FactoredSet.size_eq_prod isTrivialFactorization_of_isFactorization
  FactoredSet.dim_spec
  -- §3.1-§3.2: generation and history (FiniteFactoredSets/History.lean).  `history_isLeast`
  -- and `history_spec` are the endpoints that carry `[Finite F.B]` — finite *dimension*
  -- only, per `dd:finiteness-minimal`; nothing here assumes `S` finite.
  FactoredSet.Generates FactoredSet.generates_tfae FactoredSet.generates_spec
  FactoredSet.history FactoredSet.history_isLeast FactoredSet.history_spec
  -- §3.3-§3.4: orthogonality and time (FiniteFactoredSets/Orthogonality.lean).
  -- Definition 18 has two carriers, one per sentence: `Orthogonal` and `Entangled`.
  FactoredSet.Orthogonal FactoredSet.Entangled
  FactoredSet.orthogonal_iff_exists FactoredSet.orthogonal_spec
  FactoredSet.Before FactoredSet.StrictlyBefore
  FactoredSet.before_iff_forall_sInf FactoredSet.before_iff_forall_orthogonal
  FactoredSet.before_spec FactoredSet.history_eq_setOf_before
  -- §4.1: subpartitions and generating a subpartition
  -- (FiniteFactoredSets/Subpartition.lean).  Definition 20's `Subpartition` is a partial
  -- equivalence relation on `S` (`dd:subpartition`), Definition 21 is its `dom`, and
  -- Definition 22 is `restrict`; `GeneratesSub` is Definition 23.  As in §3.1, `C ⊆ B` is a
  -- hypothesis only where it is load-bearing — the `7 → 1` leg of Proposition 20.
  Subpartition Subpartition.dom Subpartition.restrict
  FactoredSet.GeneratesSub FactoredSet.generatesSub_tfae FactoredSet.generatesSub_spec
  -- §4.2: the history of a subpartition (FiniteFactoredSets/SubpartitionHistory.lean).
  -- `historySub` is Definition 24; Proposition 22 is the pair "least generating subset"
  -- plus "agrees with Definition 17 on partitions of `S`", so it is one endpoint with two
  -- conjuncts.  Lemmas 1 and 2 are the paper's two `lemma2`-numbered results.
  FactoredSet.historySub FactoredSet.historySub_isLeast_and_eq_history
  FactoredSet.historySub_spec FactoredSet.historySub_restrict_part_eq
  FactoredSet.historySub_inf_eq
  -- §4.3: conditional orthogonality (FiniteFactoredSets/ConditionalOrthogonality.lean).
  -- Definition 25 has three carriers, one per clause, as Definition 19 does.
  FactoredSet.OrthogonalSub FactoredSet.BeforeSub FactoredSet.StrictlyBeforeSub
  FactoredSet.OrthogonalGivenSet FactoredSet.OrthogonalGiven
  FactoredSet.orthogonal_iff_orthogonalGiven_top FactoredSet.orthogonalGiven_semigraphoid
  FactoredSet.orthogonalGiven_self_iff
  -- §5.1: characteristic polynomials (FiniteFactoredSets/Polynomial.lean).  `dd:poly` fixes
  -- the ring: `Poly^F` is `MvPolynomial (Set S) ℝ`, because under `dd:partition` a block
  -- `[s]_b` *is* the set `part b s` and so is a variable verbatim.  Definitions 29 and 30
  -- (evaluation `p(f)`, support `supp(p)`) have no declaration of ours — they are
  -- `MvPolynomial.eval` and `MvPolynomial.vars`, so they belong in the README's table of
  -- Mathlib-rendered nodes.  This is the first block that needs `[Finite S]` rather than
  -- `Finite F.B`: `Q^F_E` sums over `E ⊆ S`, so it is the intended polynomial only for
  -- finite `E`.  Not every statement here does, though — per `dd:finiteness-minimal` each
  -- carries what its own proof consumes, and Proposition 26 (`Q_eq_poly`) needs only
  -- `Finite F.B`, its content over an infinite `E` being the degenerate `0 = 0`.
  -- Propositions 27 and 28 are the two here that genuinely need `[Finite S]`, and 28
  -- (`factor2`) is the load-bearing result the rest of §5 routes through.
  Poly FactoredSet.Q mono monos poly
  FactoredSet.Q_eq_poly FactoredSet.poly_union_chimeraImage
  FactoredSet.eq_C_mul_poly_of_dvd_Q
  -- §5.3: characteristic polynomials and orthogonality
  -- (FiniteFactoredSets/CharacteristicOrthogonality.lean).  Lemma 3 (`CPO`) is a single
  -- three-clause `TFAE`, so it is one endpoint; the two isolated directions
  -- `Q_mul_Q_eq_of_orthogonalGiven` and `orthogonalGiven_of_Q_mul_Q_eq` are projections of
  -- it, on the consumer surface rather than the paper-node inventory.  The `2 → 1` leg is
  -- the one place §5 uses that `Poly^F` is a unique factorization monoid (Mathlib's
  -- `MvPolynomial.uniqueFactorizationMonoid`), which is what turns Proposition 31's
  -- irreducible factor into a prime.
  FactoredSet.orthogonalGiven_tfae
  -- Non-vacuity witnesses (FiniteFactoredSets/Examples.lean).  Every §2-§5.2 endpoint is
  -- stated over `FactoredSet`; these are what make those endpoints say something.
  -- `coordFS` is the load-bearing one: with a single factor every `C` behaves as `∅` or
  -- `B`, so Proposition 4 would be near-tautologous — and with a single factor there is no
  -- subset of `S` on which the §4 restrictions can pull apart or entangle two factors,
  -- which is what the §4 block at the end of this list needs, nor any nontrivial disjoint
  -- split of `B` for Proposition 27 or nontrivial `Irr^F(E)` for Propositions 29-31.
  Examples.bool_isFactorization Examples.boolFS
  Examples.coord_isFactorization Examples.coordFS
  Examples.not_subsingleton_coordFS_basis Examples.coordFS_chimera_corners
  Examples.empty_isFactorization Examples.emptyFS
  Examples.not_isFactorization_empty_basis
  Examples.unit_isFactorization Examples.unitFS Examples.unitFS_basis_unique
  -- Definition 10's two fields are independent: each of these exhibits one field holding
  -- while the other fails, so neither is decoration.
  Examples.not_isFactorization_singleton_fstFactor
  Examples.not_isFactorization_unit_singleton_top
  -- §2.5 on `coordFS` / `boolFS`: Propositions 7-9 applied to a concrete factored set.
  Examples.size_coordFS Examples.dim_coordFS
  Examples.size_eq_prod_coordFS Examples.dim_spec_coordFS Examples.boolFS_trivial
  -- §3 on `coordFS`: the three histories that pin the order down, then each §3 relation
  -- exhibited both holding and failing, so that none of `Generates`, `Orthogonal`,
  -- `Entangled`, `Before`, `StrictlyBefore` is silently empty or silently total.
  Examples.generates_singleton_fstFactor
  Examples.history_fstFactor Examples.history_sndFactor
  Examples.history_top Examples.history_bot Examples.history_eq_basis_of
  Examples.orthogonal_fstFactor_sndFactor Examples.not_orthogonal_fstFactor_self
  Examples.not_orthogonal_bot_fstFactor
  Examples.before_fstFactor_bot Examples.strictlyBefore_fstFactor_bot
  Examples.not_before_fstFactor_sndFactor Examples.history_eq_setOf_before_coordFS
  -- The XOR partition: `history` is not injective, so Proposition 18's `Before` is a
  -- preorder and *not* antisymmetric — which is why Proposition 18 claims no more.
  Examples.xorPart Examples.history_xorPart Examples.history_not_injective
  Examples.before_xorPart_bot_and_back Examples.entangled_xorPart_fstFactor
  -- `emptyFS`: the `Nonempty S` hypothesis on Proposition 13 clause 4 and Proposition 19
  -- is load-bearing — both conclusions fail outright over the empty set.
  Examples.emptyFS_history_bot Examples.emptyFS_history_ne_singleton
  Examples.emptyFS_history_ne_setOf_before
  -- §4 on `coordFS`: the two coordinate factors restricted to a block of `fstFactor`
  -- (`Efst`, where they stay independent) and to the diagonal (`Ediag`, a block of
  -- `xorPart`, where the first coordinate determines the second).  Domains, blocks,
  -- `GeneratesSub`, `historySub` and conditional orthogonality are computed over both.
  Examples.Efst Examples.Ediag Examples.sndOnEfst
  Examples.classes_sndOnEfst Examples.generatesSub_sndOnEfst
  Examples.not_generatesSub_fst_sndOnEfst Examples.historySub_sndOnEfst
  Examples.generatesSub_tfae_on_sndOnEfst Examples.generatesSub_iff_on_sndOnEfst
  -- Generation of a subpartition is not monotone in `C` (the paper's remark after
  -- Proposition 21), so Proposition 20 clause 7's second conjunct is load-bearing.
  Examples.indDiag Examples.historySub_indDiag Examples.generatesSub_empty_indDiag
  Examples.not_generatesSub_fst_indDiag Examples.generatesSub_not_superset_monotone
  Examples.clause7_second_conjunct_loadbearing
  -- `hE : X.dom = Y.dom` in Proposition 23 clause 2 is load-bearing, and the history it
  -- computes is the nondegenerate `{sndFactor}` rather than `∅`.
  Examples.Efalse Examples.botInfIndEfalse Examples.historySub_botInfIndEfalse
  Examples.historySub_spec_hE_loadbearing
  -- `Subset` (inclusion as sets of blocks) both ways, and `dd:subpartition`'s bijection
  -- with `Σ E, Setoid E` exhibited on a concrete `E`.
  Examples.subset_indDiag_xorPart Examples.not_subset_sndOnEfst_snd
  Examples.ofSetoidOn_bot_Efst Examples.roundtrip_sndOnEfst Examples.roundtrip_bot_Efst
  Examples.restrict_restrict_sndOnEfst
  -- Lemmas 1 and 2 instantiated: their hypothesis sets are satisfiable, and Lemma 2's two
  -- sides are each computed to `B` without invoking Lemma 2 (the left from Proposition 22,
  -- the right from Lemma 1), so the pair cross-checks Lemma 2 on the witness.
  Examples.historySub_ofSetoid_fstFactor Examples.historySub_ofSetoid_sndFactor
  Examples.historySub_disjoint_coord Examples.lemma1_coordFS Examples.lemma1_coordFS'
  Examples.lemma2_lhs_coordFS Examples.lemma2_rhs_coordFS
  -- §4.3: restriction can entangle, so `OrthogonalGiven` is neither empty nor total and is
  -- not implied by Definition 18; Proposition 25 exhibited on the witness, and Theorem 2
  -- largely so.  Read the Theorem 2 witnesses for exactly what they are: the two
  -- instances here are degenerate on purpose (`thm2_decomposition_coordFS` takes `W = ⊤`,
  -- `thm2_weakUnion_coordFS` takes `W = Y`); the non-degenerate decomposition,
  -- contraction and composition instances are in the block below.  The endpoint
  -- `orthogonalGiven_semigraphoid` carries all five clauses; the witnesses meter four
  -- (symmetry has no dedicated instance).
  Examples.fstOnEdiag Examples.sndOnEdiag
  Examples.historySub_fstOnEdiag Examples.historySub_sndOnEdiag
  Examples.not_orthogonalGivenSet_Ediag Examples.Ediag_mem_xorPart_classes
  Examples.not_orthogonalGiven_fst_snd_xorPart Examples.orthogonalGiven_fst_snd_top
  Examples.orthogonalGiven_nondegenerate Examples.not_orthogonalGiven_fst_fst_top
  Examples.orthogonalGiven_fst_fst_fst
  Examples.thm2_decomposition_coordFS Examples.thm2_weakUnion_coordFS
  -- Those two are instantiated at degenerate arguments (`W = ⊤`, resp. `W = Y`), so each
  -- of their conclusions is a fact §4.3 already has; their docstrings say so.  The
  -- non-degenerate instance conditions on `xorPart` and needs partitions of *mixed* type,
  -- because `fstFactor`, `sndFactor`, `xorPart`, `Dis_S` and `Ind_S` each restrict
  -- uniformly — all-discrete or all-indiscrete — to the two blocks of any 2+2 partition, so
  -- no two of them can trade roles across blocks.  `diagPart`, `orPart` and `andPart` do
  -- trade: `orthogonalGiven_diagPart_orAnd_xorPart` is `X ⊥^F (Y ∨_S W) | Z` with the left
  -- argument carrying the diagonal block and the right the antidiagonal one, certified
  -- two-sided by `orthogonalGiven_diagPart_orAnd_xorPart_two_sided` — neither restricted
  -- history is empty on both blocks — so Theorem 2's decomposition, contraction and
  -- composition clauses all do work on it.  Clauses 4 and 5 had no concrete instance
  -- before; their second input is the auxiliary `diagPart ⊥^F xorPart | Z`, so neither is
  -- the decomposition run backwards.
  Examples.diagPart Examples.orPart Examples.andPart
  Examples.orthogonalGiven_diagPart_orAnd_xorPart
  Examples.orthogonalGiven_diagPart_orAnd_xorPart_two_sided
  Examples.thm2_decomposition_coordFS_xorPart Examples.thm2_contraction_coordFS
  Examples.thm2_composition_coordFS
  -- The degenerate corners of Definitions 26-27, recorded so a client does not rediscover
  -- them: conditioning on `∅` or on `Dis_S` makes every pair orthogonal.
  Examples.orthogonalGivenSet_empty Examples.orthogonalGiven_bot
  -- §5.2: factoring the characteristic polynomial (FiniteFactoredSets/Factoring.lean).
  -- `irr` is Definition 35; Proposition 29 is the triple "members nonempty, pairwise
  -- disjoint, cover `B`", which under `dd:partition` is what "is a partition of the set
  -- `B`" means (`irr_isPartition` restates it as a `Subpartition`, and is machinery rather
  -- than a node).  Propositions 30 and 31 together are the factorization of `Q^F_E` into
  -- irreducibles.  Propositions 30 and 31 are where `[Finite S]` — finite *size*, not just
  -- finite dimension — is genuinely consumed, for the reason recorded under `dd:poly`.
  -- Proposition 29 is not: its proof is the minimal-element argument over subsets of `B`
  -- plus the `chimeraImage` closure lemmas, so it carries `Finite F.B` alone and holds
  -- over an infinite `S` — and, unlike the §5.1 relaxations, non-degenerately.
  FactoredSet.irr FactoredSet.irr_partition
  FactoredSet.Q_eq_finprod_poly_irr FactoredSet.irreducible_poly_of_mem_irr
  -- §5.4-§5.5: probability and the fundamental theorem
  -- (FiniteFactoredSets/Probability.lean).  Definition 36 is `ProbDist`, the paper's own
  -- elementary four-clause structure on `𝒫(S) → ℝ` (`dd:probability`; no measure theory
  -- stands in for it), and Definition 37 is the predicate `IsDistribution` on one.  Both
  -- §5.4-§5.5 theorems carry `[Finite S]`: Proposition 32 sums over `E ⊆ S`, and Theorem 3
  -- routes through Lemma 3, so this is the same `dd:poly` boundary as §5.1-§5.2 rather
  -- than a new hypothesis.  Theorem 3's converse is the only paper-node proof that
  -- *constructs* a distribution rather than quantifying over one — the paper's `P_f`, built
  -- from a strictly positive weight function — so the two directions have genuinely
  -- different content.  (The consumer surface also supplies `ProbDist.diracAt`, and
  -- `Examples` builds `uniform`, `biased`, `diagDist`, `unitDist` and `boolUniform`; none
  -- of those is a paper node.)
  ProbDist FactoredSet.IsDistribution
  FactoredSet.isDistribution_iff FactoredSet.orthogonalGiven_iff_forall_isDistribution
  -- §5.1-§5.2 on `coordFS`: the characteristic polynomial computed outright.  `vfst`/`vsnd`
  -- are the four variables of `Poly^{coordFS}` that ever occur — under `dd:partition` a
  -- block *is* a subset of `S`, hence a variable of the ring verbatim.  `Q_coordFS_univ_eq`
  -- expands Definition 31 to a four-term polynomial with no `finsum`/`finprod` left, and
  -- the two facts beside it rule out the degenerate readings: `Q^F_S` is not `0`, and no
  -- variable has degree above one in it (Corollary 1 at work).
  Examples.vfst Examples.vsnd
  Examples.Q_coordFS_univ_eq Examples.Q_coordFS_univ_ne_zero
  Examples.degreeOf_Q_coordFS_univ_le_one
  -- Definition 33 is an *image*, so coincident monomials collapse: `S` has four points and
  -- `poly^F_{fst}(S)` has two summands.  That collapse is the subtlety Proposition 26 has
  -- to rule out at `C = B`, and `mono_coordFS_basis_injective` is the ruling-out on the
  -- witness (proved by separating evaluation, not by citing Proposition 3).
  Examples.mono_singleton_fst_true_false
  Examples.poly_singleton_fst_univ Examples.poly_singleton_snd_univ
  Examples.mono_coordFS_basis_injective
  -- Proposition 26 on the witness, as a cross-check pair plus a separate application:
  -- `Q_coordFS_univ_eq` and `poly_coordFS_basis_univ_eq` each compute their own side to
  -- the same explicit polynomial and neither mentions `Q_eq_poly`, so
  -- `prop26_coordFS_crosscheck` re-derives the proposition rather than echoing it;
  -- `prop26_coordFS_applied` is the endpoint instantiated, which is a different claim.
  Examples.poly_coordFS_basis_univ_eq
  Examples.prop26_coordFS_crosscheck Examples.prop26_coordFS_applied
  -- Definition 35 computed at two subsets, with different answers.  At `E = S` the
  -- irreducible parts are the two singletons (the minimality clause is *vacuous* at a
  -- singleton — `∅` is the only strict subset and it is not nonempty — so what excludes
  -- `C = B` is that `{fstFactor}` already fixes `S`).  On the diagonal neither coordinate
  -- alone fixes `Ediag`, so the only irreducible part is the whole basis: the §5 shadow of
  -- the §4 fact that restriction entangles.
  Examples.mem_irr_singleton_fst_univ Examples.mem_irr_singleton_snd_univ
  Examples.irr_coordFS_univ
  Examples.chimeraImage_singleton_fst_Ediag_ne Examples.chimeraImage_singleton_snd_Ediag_ne
  Examples.irr_coordFS_Ediag
  -- Proposition 30 on the witness, the same cross-check shape: the factorization at `E = S`
  -- computed by expanding both sides (no mention of `Q_eq_finprod_poly_irr`), beside the
  -- endpoint applied at `S` and at `Ediag`, where the product degenerates to one factor and
  -- so agrees with Proposition 26 there.
  Examples.Q_coordFS_univ_eq_mul_poly
  Examples.prop30_coordFS_univ_applied Examples.prop30_coordFS_Ediag_applied
  -- §5 at `E = Efst`, a *third* subset, where Definitions 31 and 34 take values distinct
  -- from both earlier ones: `poly^F_{fst}(Efst)` collapses to one variable while
  -- `poly^F_{snd}(Efst)` keeps two, so Propositions 26 and 30 factor `Q^F_{Efst}` into two
  -- *different* polynomials (at `E = S` the two factors are symmetric; at `Ediag` there is
  -- one).  `Irr^F(Efst)` is the two singletons again — so `Irr^F` agreeing at two subsets
  -- does not mean the factorizations do.
  Examples.poly_singleton_fst_Efst Examples.poly_singleton_snd_Efst
  Examples.Q_coordFS_Efst_eq Examples.poly_coordFS_basis_Efst_eq
  Examples.prop26_coordFS_Efst_applied Examples.prop26_coordFS_Efst_crosscheck
  Examples.irr_coordFS_Efst
  Examples.prop30_coordFS_Efst_applied Examples.prop30_coordFS_Efst_crosscheck
  -- Proposition 27 at a nontrivial split — `C₀ = {fstFactor}`, `C₁ = {sndFactor}` disjoint
  -- and nonempty with `C₀ ∪ C₁ = B`, and `E₀ = Efst ≠ S = E₁` — applied, cross-checked by
  -- computation (no mention of `poly_union_chimeraImage`), and with the chimera's argument
  -- order pinned executably: the reversed reading `χ^F_{C₀}(E₁, E₀)` is *false* here.
  Examples.prop27_coordFS_applied Examples.prop27_coordFS_crosscheck
  Examples.prop27_reversed_false
  -- Proposition 28 is not vacuous on the witness, and its conclusion is doing work.
  -- `poly^F_{fst}(S)` really divides `Q^F_S` (computed, not via the endpoint).  The
  -- conclusion's `r · poly^F_C(E)` shape is *not* inventoried at that divisor, because
  -- asserting it at a `poly^F_C(E)` is a triviality — provable for every `C ⊆ B` and every
  -- `E` with none of the proposition's hypotheses (the `example` beside the divisor in
  -- Examples.lean is the probe).  The informative instances are the two below: at
  -- `2 · poly^F_{fst}(S)` the divisor is no `poly^F_C(S)` at all, so the real coefficient
  -- `r` cannot be dropped; and at a nonzero constant the returned `C` is forced to `∅`.
  Examples.poly_singleton_fst_dvd_Q_coordFS_univ
  Examples.prop28_coordFS_scaled_applied Examples.prop28_r_loadbearing
  Examples.prop28_coordFS_const_applied Examples.prop28_const_forces_empty
  -- Proposition 29 applied at both computed subsets, each cross-checked against the
  -- computed `Irr^F` without mentioning `irr_partition`; and its §4 restatement
  -- `irr_isPartition` instantiated, so the `Subpartition` it promises is constructed.
  -- The two cross-checks state the endpoint's own third conjunct, `⋃₀ Irr^F(E) = B`, and
  -- reach it by rewriting with the computed `Irr^F(E)`; they are not the generic set
  -- identities `⋃₀ {{fst}, {snd}} = B` / `⋃₀ {B} = B`, which mention no `Irr^F` and so
  -- would check nothing.
  Examples.prop29_coordFS_univ_applied Examples.sUnion_irr_coordFS_univ_crosscheck
  Examples.prop29_coordFS_Ediag_applied Examples.sUnion_irr_coordFS_Ediag_crosscheck
  Examples.irr_isPartition_coordFS_univ_applied
  -- Proposition 31 applied to both irreducible parts, with the two negatives that stop it
  -- being vacuous: neither factor is a unit, and `Irreducible` is not total on this ring —
  -- `Q^F_S` itself is reducible.
  Examples.prop31_coordFS_fst_applied Examples.prop31_coordFS_snd_applied
  Examples.not_isUnit_poly_singleton_fst_univ Examples.not_isUnit_poly_singleton_snd_univ
  Examples.not_irreducible_Q_coordFS_univ
  -- The three §5.1 endpoints the computed facts above shadow but never instantiate,
  -- applied on the witness.
  Examples.Q_ne_zero_coordFS_applied Examples.degreeOf_Q_le_coordFS_applied
  Examples.vars_disjoint_coordFS_applied
  -- The `E.Nonempty` hypotheses of §5 are load-bearing: at `E = ∅` both `Q^F_∅` and every
  -- `poly^F_C(∅)` are `0`, and Propositions 28, 30 and 31 each fail outright (30's on the
  -- zero-dimensional `unitFS`, where `Irr^F(∅) = ∅` makes the product `1`).  Proposition
  -- 29's `hE` is the exception, and `irr_partition_holds_at_empty` is the computation
  -- backing that disclosure rather than a load-bearing claim: it states all three of
  -- Proposition 29's conjuncts at `E = ∅`, computed from `irr_coordFS_empty`.
  Examples.poly_empty_eq_zero Examples.Q_coordFS_empty Examples.irr_coordFS_empty
  Examples.irr_partition_holds_at_empty
  Examples.prop28_hE_loadbearing Examples.prop30_hE_loadbearing
  Examples.prop31_hE_loadbearing
  -- `poly` is total in `C`, so it takes a junk value off the paper's `C ⊆ B`.  Recorded so
  -- that nobody reads a §5 statement as covering it: at `C = {Ind_S}` it is a single
  -- variable, and `Ind_S ∉ B`, so no §5.1-§5.2 hypothesis is satisfied by it.
  Examples.poly_top_univ_junk Examples.top_notMem_coordFS_basis
  -- §5.3-§5.5 on `coordFS`: Definition 31 at the remaining blocks Lemma 3 and Theorem
  -- 3 quantify over — the singleton `{s}`, every block of each coordinate factor (with the
  -- `sndFactor` block `[·]₂ = true` named separately, since the §5.3 witnesses run at it),
  -- and the diagonal `Ediag`, which is where both verdicts flip.
  Examples.Q_coordFS_singleton Examples.Q_coordFS_vfst Examples.Q_coordFS_vsnd
  Examples.Q_coordFS_vsnd_true Examples.Q_coordFS_Ediag
  -- Lemma 3's clause 3 on the witness, as a cross-check pair plus a separate application,
  -- and the negative that stops it being a triviality.  The cross-check expands both
  -- products from Definition 31 and mentions no divisibility endpoint; the application
  -- feeds the §4.3 fact `fstFactor ⊥^F sndFactor | Ind_S` to Lemma 3's 1 → 3 direction.
  -- At the `xorPart` block `Ediag` clause 3 *fails*, separated by one `coordSep`
  -- evaluation (310 against 100) — the polynomial shadow of §4.3's entanglement.
  Examples.lemma3_clause3_coordFS_top_crosscheck
  Examples.lemma3_clause3_coordFS_top_applied
  Examples.lemma3_clause3_coordFS_Ediag_fails
  -- Lemma 3's clause 2 — the divisibility, which is reachable only through the `TFAE` —
  -- at the same two conditionings.  The cross-check exhibits the cofactor `Q^F_{(t,t)}`
  -- computed from Definition 31 and states the same divisibility the application projects
  -- with `.out 0 1`; on the diagonal divisibility fails, refuted by a single *zero* of the
  -- divisor (`coordZero`) rather than by the separating value `coordSep` supplies for
  -- clause 3.
  Examples.lemma3_clause2_top_crosscheck Examples.lemma3_clause2_top_applied
  Examples.lemma3_clause2_Ediag_fails
  -- Lemma 3's `3 → 1` direction run FORWARD, with its hypothesis discharged by computing
  -- clause 3 at every pair of blocks rather than assumed or contraposed.  This is the
  -- direction §5.5 consumes, and `orthogonalGiven_from_clause3` reaches
  -- `fstFactor ⊥^F sndFactor | Ind_S` by a route independent of Proposition 24's.
  Examples.clause3_fst_snd_top Examples.orthogonalGiven_from_clause3
  -- Definitions 36 and 37 inhabited, kept apart, and kept from naming one distribution.
  -- `uniform` (`P E = |E| / 4`) and `biased` (a product of two `1/3`-biased coins) are two
  -- *different* distributions on the factored set; `diagDist` (`P E = |E ∩ Ediag| / 2`) is
  -- a `ProbDist` and is *not* one, since it makes the two coordinates perfectly correlated
  -- (`P {(t,t)} = 1/2` against `P([s]_fst) · P([s]_snd) = 1/4`).  Without `diagDist`,
  -- Definition 37's product condition would be indistinguishable from decoration; without
  -- `uniform` and `biased`, Proposition 32 and Theorem 3 would have no exhibited
  -- inhabitant to quantify over here.  (The family is not in fact empty for any nonempty
  -- `S`: the point mass is a distribution on every factored set of finite dimension,
  -- `FactoredSet.isDistribution_diracAt` in the conveniences block below.  What the
  -- witnesses supply is a *computed* inhabitant, and a second one that is not the first.)
  Examples.uniform Examples.uniform_isDistribution
  Examples.biased Examples.biased_isDistribution Examples.biased_ne_uniform
  Examples.diagDist Examples.not_isDistribution_diagDist
  -- Proposition 32 at two subsets and under two distributions.  At `E = Efst` the
  -- polynomial has two terms, so the evaluation is a genuine sum — equal summands under
  -- `uniform`, unequal ones under `biased`; at the three-element `E3` it has three terms
  -- taking two distinct values.  Each is cross-checked by computing both sides from
  -- Definitions 31 and 36, and separately applied.
  Examples.prop32_coordFS_Efst_crosscheck Examples.prop32_coordFS_Efst_applied
  Examples.prop32_biased_Efst_crosscheck Examples.prop32_biased_Efst_applied
  Examples.E3 Examples.Q_coordFS_E3
  Examples.prop32_biased_E3_crosscheck Examples.prop32_biased_E3_applied
  -- Theorem 3 in both directions on the pair §4.3 already separates.  Forward at
  -- `Z = Ind_S`: cross-checked (`1/2 · 1/2 = 1/4 · 1`, computed) and applied (from
  -- `orthogonalGiven_fst_snd_top`, with no computation).  Backward at `Z = xorPart`:
  -- `thm3_coordFS_Ediag_fails` computes the failure (`1/16` against `1/8`),
  -- `thm3_coordFS_xorPart_witness` names the distribution and blocks realizing the
  -- theorem's existential, and `thm3_coordFS_xorPart_applied` derives that same
  -- existential from `not_orthogonalGiven_fst_snd_xorPart` through the endpoint.
  Examples.thm3_coordFS_top_crosscheck Examples.thm3_coordFS_top_applied
  Examples.thm3_coordFS_Ediag_fails
  Examples.thm3_coordFS_xorPart_witness Examples.thm3_coordFS_xorPart_applied
  -- Theorem 3's converse run FORWARD as well: independence in every distribution on
  -- `coordFS`, obtained from `clause3_fst_snd_top` through Proposition 32 without invoking
  -- Lemma 3 or Theorem 3's forward direction, yields conditional orthogonality.  This is
  -- the third independent derivation of `fstFactor ⊥^F sndFactor | Ind_S` in the file.
  Examples.orthogonalGiven_from_independence
  -- The degenerate carriers of Definitions 36-37, which say where the quantifiers of
  -- Proposition 32 and Theorem 3 are and are not vacuous.  Over `Empty` there is no
  -- distribution at all, and both sides of Theorem 3 hold there (a partition of `∅` has no
  -- blocks) — so the theorem is consistent, not informative.  Over `Unit` there is exactly
  -- one distribution, and it *is* a distribution on the zero-dimensional `unitFS`, the
  -- empty product being `1`.
  Examples.isEmpty_probDist_empty Examples.orthogonalGiven_emptyFS
  Examples.unitDist Examples.subsingleton_probDist_unit Examples.unitDist_isDistribution
  -- …and Theorem 3's right-hand side is not universally true: one dimension suffices.  On
  -- `boolFS` every `ProbDist Bool` is a distribution on the factored set (`B = {Dis_S}`
  -- makes Definition 37 no constraint), and the uniform one refutes `Dis_S ⊥^F Dis_S |
  -- Ind_S` — `1/2 · 1/2` against `0 · 1`.
  Examples.boolUniform Examples.boolFS_isDistribution
  Examples.not_orthogonalGiven_bot_bot_top_boolFS
  -- §7.2: Conjecture 1 (FiniteFactoredSets/Conjecture.lean) and its finite-dimensional /
  -- infinite-dimensional witnesses (FiniteFactoredSets/InfiniteExamples.lean).
  -- `FundamentalTheoremFiniteDim` is a `def … : Prop` — Theorem 3 with `[Finite S]` weakened
  -- to `[Finite F.B]` — and is deliberately **not proved**: no declaration in the repo has
  -- that type.  It is used in exactly three places, each an `example` that takes it *as a
  -- hypothesis* and instantiates it at a witness: two in `InfiniteExamples` and one in
  -- `APITests/FiniteFactoredSets.lean`, the last being the client-side half.  So listing it here
  -- checks the statement's own axiom profile, exactly as the block already does for the
  -- other `def … : Prop`s above (`OrthDatabase.Consistent`, `FactoredSet.Generates`).  Its
  -- finite restriction needs no declaration of its own: it *is* Theorem 3
  -- (`FactoredSet.orthogonalGiven_iff_forall_isDistribution`, inventoried above).
  FundamentalTheoremFiniteDim
  -- The witnesses.  `natBoolFS` is dimension 2 over the *infinite* carrier `ℕ × Bool`, so
  -- `Finite natBoolFS.B` holds (by `Set.Finite.to_subtype`, not by Proposition 6, which
  -- runs the other way) while `¬ Finite (ℕ × Bool)`: it is inside Conjecture 1's scope and
  -- outside Theorem 3's, which is what stops the conjecture from being a restatement of
  -- the theorem.  §3-§4 is then run on it — Proposition 13 clause 4 for both factor
  -- histories, Definition 18 computed from those histories, Proposition 14 as an
  -- independent re-derivation, Proposition 15 clause 4 as the negative, Proposition 24 for
  -- Definition 27 at `Ind_S` — with `Finite B` alone and no `Finite S` anywhere, which is
  -- `dd:finiteness-minimal` discharged by construction rather than by inspection.
  -- `isDistribution_diracAt_natBoolFS` makes Definition 37 inhabited there, but
  -- inhabitation is not what makes the conjecture's right-hand side a constraint:
  -- `diracAt_rhs_trivial` shows a point mass satisfies Theorem 3's right-hand-side identity
  -- for *arbitrary* sets, so a dirac-only family would make that side constantly true and,
  -- against `not_orthogonal_natFactor_self`, would refute Conjecture 1 rather than exhibit
  -- it.  `rich` — uniform on the four points `{0,1} × Bool` — is the discriminating member:
  -- a Definition-37 distribution on `natBoolFS` (`rich_isDistribution`) that falsifies the
  -- right-hand-side clause in the shape the conjecture quantifies it
  -- (`rich_discriminates`), so `both_sides_fail_at_natFactor_self` computes both sides of
  -- the biconditional at one triple.  This is the infinite-carrier counterpart of
  -- `Examples.not_orthogonalGiven_bot_bot_top_boolFS`.
  InfiniteExamples.natFactor InfiniteExamples.boolFactor
  InfiniteExamples.natFactor_ne_boolFactor InfiniteExamples.natBoolBasis
  InfiniteExamples.natBoolBasis_nontrivial InfiniteExamples.natBoolBasis_existsUnique
  InfiniteExamples.natBool_isFactorization InfiniteExamples.natBoolFS
  InfiniteExamples.natBoolFS_B InfiniteExamples.natFactor_mem
  InfiniteExamples.boolFactor_mem InfiniteExamples.singleton_natFactor_subset
  InfiniteExamples.singleton_boolFactor_subset InfiniteExamples.natBoolFS_B_finite
  InfiniteExamples.not_finite_natBool
  InfiniteExamples.finSupp InfiniteExamples.finSupp_rel_iff InfiniteExamples.finSupp_ne_top
  InfiniteExamples.history_finSupp InfiniteExamples.orthogonal_finSupp_self
  InfiniteExamples.history_natFactor InfiniteExamples.history_boolFactor
  InfiniteExamples.orthogonal_natFactor_boolFactor
  InfiniteExamples.not_orthogonal_natFactor_self
  InfiniteExamples.orthogonalGiven_natFactor_boolFactor_top
  InfiniteExamples.isDistribution_diracAt_natBoolFS
  InfiniteExamples.diracAt_rhs_trivial InfiniteExamples.richSupport InfiniteExamples.rich
  InfiniteExamples.rich_apply InfiniteExamples.rich_isDistribution
  InfiniteExamples.rich_discriminates InfiniteExamples.both_sides_fail_at_natFactor_self
  -- `infFS` is the other side of the line: the coordinate factorization of `ℕ → Bool`,
  -- whose basis is infinite (`infFS_B_infinite`, `not_finite_B`).  Up to
  -- `𝒫(ℕ) ≃ (ℕ → Bool)` it is the factored set §7.2 uses to say it does *not* expect the
  -- fundamental theorem past finite dimension.  It is the `F` of both §7.2 examples:
  -- Example 3 is out of scope by ruling, while Example 4 (in scope since 2026-08-30) is
  -- carried by `infFS` with `finSupp` / `finSupp_ne_top` / `orthogonal_finSupp_self`
  -- below.  `not_isDistribution_diracAt_infFS` is what makes the conjecture-boundary
  -- reading earn its place: the
  -- `[Finite F.B]` on `FactoredSet.isDistribution_diracAt` is load-bearing, because with
  -- `B` infinite the family in Definition 37 has infinite multiplicative support and
  -- `finprod` returns `1` rather than the elementary product.  So past finite dimension
  -- Definition 37's product is not the product it is written as — the concrete reason the
  -- conjecture is stated at finite dimension and not beyond.  The second reason is
  -- `not_isLeast_history_evEq`: **Proposition 12's conclusion is false** on `infFS`.  For
  -- the eventually-equal partition `evEq`, dropping any single coordinate from `B` still
  -- generates it, so `h^F(evEq) = ∅` (`history_evEq`) while `∅` generates only `Ind_S` and
  -- `evEq ≠ Ind_S` (`evEq_ne_top`).  So `[Finite F.B]` on `FactoredSet.history_isLeast` is
  -- load-bearing, and past finite dimension `history` is defined but is no longer the
  -- object §3.2 onwards reasons about — the justification `History.lean`'s module doc gives
  -- for that binder is now compiled rather than asserted.
  InfiniteExamples.memFactor InfiniteExamples.infBasis
  InfiniteExamples.memFactor_injective InfiniteExamples.infBasis_nontrivial
  InfiniteExamples.infBasis_existsUnique InfiniteExamples.infFS
  InfiniteExamples.infFS_B InfiniteExamples.infFS_B_infinite
  InfiniteExamples.not_finite_B
  InfiniteExamples.not_isDistribution_diracAt_infFS
  InfiniteExamples.evEq InfiniteExamples.evEq_ne_top InfiniteExamples.history_evEq
  InfiniteExamples.not_generates_history_evEq InfiniteExamples.not_isLeast_history_evEq
  -- §6.1: factored set models and orthogonality databases
  -- (FiniteFactoredSets/Inference.lean).  Definition 38's `Model` bundles the carrier, its
  -- factored set, the map to `Ω`, and — because the paper says *finite* factored set — a
  -- `Finite` field, so Definition 45's quantifier over models is the paper's (`dd:model`).
  -- One precision: `Model : Type u → Type (u+1)` puts the carrier `S` in `Ω`'s own
  -- universe, so "every model" below means every model with a `Type u` carrier.  That is
  -- forced by Lean and mathematically empty — every carrier is finite, hence equivalent to
  -- one in `Type 0` — but the repo has no transport lemma along such an equivalence, so it
  -- is disclosed rather than discharged (`dd:model`).
  -- Definition 39's three preimages are Mathlib-rendered (README table); `Model.pullback`
  -- names the partition one and is a convenience, not a paper endpoint.  Definition 41 has
  -- two carriers, one per written form, as Definitions 18 and 19 do.  `Model` is spelled
  -- with its root prefix: `ProvabilityLogic/Kripke/Basic.lean` declares a root-namespace
  -- `Model`, so the bare name is ambiguous under this block's `open FiniteFactoredSets in`.
  FiniteFactoredSets.Model OrthDatabase OrthDatabase.Orth OrthDatabase.NotOrth
  OrthDatabase.Models OrthDatabase.Consistent OrthDatabase.Complete OrthDatabase.StrictlyBefore
  -- §6.2, Example 1 (FiniteFactoredSets/InferenceExamples.lean).  `Example1.D` is the
  -- database of the worked example; Propositions 33 and 34 are consistency (witnessed by
  -- the identity model on `(Ω, {X, V})`) and the inferred order `X <_D Y`, which quantifies
  -- over every model of `D` — in the §6.1 sense above, `Type u` carriers — and so is a
  -- universal claim, not an instantiated one.
  Example1.D Example1.D_consistent Example1.strictlyBefore_X_Y
  -- §6.2, Example 2 (FiniteFactoredSets/InferenceExamples.lean).  `Example2.D` is the
  -- database of the paper's second worked example; Propositions 35 and 36 are its
  -- consistency and the temporal order it forces.  Proposition 35 is discharged by the
  -- paper's own twelve-point model — `Example2.model`, on the carrier
  -- `Bool × Bool × Option Bool` whose `none` third coordinate is the paper's two-bit
  -- string — so the existential of Definition 43 is met by a construction, not a
  -- stand-in.  Proposition 36 quantifies over every model of `D` in that same sense, so it
  -- needs no witness of its own; what makes it non-vacuous is Proposition 35, which
  -- supplies one.
  Example2.D Example2.D_consistent Example2.strictlyBefore_X_Y_Z
  -- §6.1 on the witnesses (FiniteFactoredSets/Examples.lean).  Definitions 42-45 quantify
  -- over *models* of a sample space, not over factored sets, so none of the §2-§5 witnesses
  -- above touches them.  Definition 38 is inhabited four ways: the two identity models, the
  -- non-injective `fstModel` (`coordFS` observed through `Prod.fst`, where `S` has four
  -- points and `Ω` two — the latent structure Definition 38 exists to allow), and the
  -- one-point `pointModel`.  Definition 39 is computed on the two that are not the
  -- identity, and it moves in both directions: `f⁻¹(Dis_Ω)` can be a *factor* of `S`
  -- (`pullback_fstModel_bot`, whose §3 history is the singleton) and it can collapse every
  -- partition of `Ω` to `Ind_S` (`pullback_pointModel`).
  -- `voidModel` is the fifth and degenerate end of Definition 38: the empty carrier, legal
  -- because `Model`'s `Finite S` field is satisfied by `Empty`.  It is what makes
  -- `not_strictlyBefore_of_notOrth_empty` true — it models every database whose `N` is
  -- empty, and over it every history is `∅`, so Definition 45 infers nothing.  That is the
  -- exact dual of `totalDB_consistent`: `O` costs a database no consistency and buys it no
  -- inferences, `N` does both.
  Examples.coordModel Examples.boolModel Examples.fstModel Examples.pointModel
  Examples.voidModel
  Examples.pullback_fstModel_bot Examples.history_pullback_fstModel_bot
  Examples.pullback_pointModel
  -- Definitions 40-44 on six databases.  Two natural misreadings are ruled out here.
  -- First, `Consistent` is cheap on `O` alone: `totalDB` asserts *every* triple orthogonal
  -- and is still consistent, because the one-point model satisfies all of `O` at once
  -- (`unitFS` has no factors) — so it is `N` that constrains, and
  -- `nonconstDB_forces_nonconstant` is the mechanism in its simplest form, a single
  -- `N`-entry forcing every model's map to be non-constant through Proposition 25.
  -- Second, `Consistent` and `Complete` are independent **in both directions**, and each
  -- direction is now inhabited: `emptyDB` is consistent and not complete,
  -- `completeInconsistentDB` — asserting every triple both ways — is complete and not
  -- consistent, and `totalDB` is both.  `coordDB` repeats the consistent-and-not-complete
  -- corner with both of its clauses non-empty, and `contradictoryDB` — asserting one triple
  -- both ways — has no model at all, which is what makes Definition 43's existential a real
  -- condition.
  -- `models_coordDB` is the Definition 42 computation proper, discharging both clauses on
  -- the identity model of `coordFS` from §4.3's own computations on that witness.
  Examples.emptyDB Examples.models_emptyDB Examples.emptyDB_consistent
  Examples.not_emptyDB_complete
  Examples.not_strictlyBefore_of_notOrth_empty Examples.not_emptyDB_strictlyBefore
  Examples.contradictoryDB Examples.not_contradictoryDB_consistent
  Examples.totalDB Examples.totalDB_complete Examples.totalDB_consistent
  Examples.completeInconsistentDB Examples.completeInconsistentDB_complete
  Examples.not_completeInconsistentDB_consistent
  Examples.nonconstDB Examples.nonconstDB_consistent
  Examples.nonconstDB_forces_nonconstant
  Examples.coordDB Examples.models_coordDB Examples.coordDB_consistent
  Examples.not_coordDB_complete
  -- Definition 45 from both sides.  On a *consistent* database it is irreflexive, since
  -- `<^F` is a strict inclusion of histories; on an *inconsistent* one it is vacuously
  -- total, quantifying over models that do not exist.  That second fact is the trap the
  -- paper's own ordering guards against — Propositions 33 and 35 (consistency) come before
  -- Propositions 34 and 36 (the inference).  The informative positive instances of
  -- Definition 45 are those two propositions in `InferenceExamples.lean`; nothing here
  -- stands in for them, and `Examples.lean` does not import that file.  The two generic
  -- statements these instantiate are `OrthDatabase.not_strictlyBefore_self_of_consistent` and
  -- `OrthDatabase.strictlyBefore_of_not_consistent`, on the consumer surface below.
  Examples.not_nonconstDB_strictlyBefore_self Examples.contradictoryDB_strictlyBefore_all
  -- §7.3: embedded observations, counterfactability, conditional time
  -- (FiniteFactoredSets/EmbeddedAgency.lean).  Five definitions and no theorem: §7 states
  -- nothing about them, so the whole non-vacuity burden falls on the witnesses below.
  -- Definition 46's auxiliary `X_E` is `FactoredSet.eventPartition`, which carries no node
  -- annotation and is therefore not listed here — the paper introduces it inside the
  -- statement of Definition 46 rather than as a numbered node, and it is an auxiliary in the
  -- same sense `Model.pullback` is.  Two renderings to record.  First, `eventPartition E` is
  -- `Setoid.comap (· ∈ E) ⊥` — agreement on membership in `E` — so the paper's case split
  -- (`{S}` when `E` is `∅` or `S`, `{E, S \ E}` otherwise) is absorbed into one formula and
  -- recovered by computation on the witnesses.  Second, Definition 47's family `A_i` is
  -- indexed by the *blocks* of `X` rather than by a numbering `{x_0, …, x_{n-1}}` of them,
  -- and the paper's `⋁_S({A_i})` is `sInf (Set.range ·)` (`dd:order-flip`); indexing by
  -- blocks changes nothing and needs no finiteness.  Per `dd:finiteness-minimal` none of the
  -- five carries a finiteness hypothesis — each is a formula in
  -- `history`/`historySub`/`Orthogonal`/`OrthogonalGiven`, all defined for every factored
  -- set — and Definition 50's `h^F(X | E)` is `historySub ((ofSetoid X).restrict E)`, the
  -- Definition 26 rendering reused.
  FactoredSet.Observes FactoredSet.ObservesPartition FactoredSet.Counterfactable
  FactoredSet.CounterfactableRel FactoredSet.BeforeGivenSet
  -- §7.3 on the witnesses (FiniteFactoredSets/Examples.lean).  The paper's case split for
  -- `X_E` is recovered in three pieces: `Ind_S` at both degenerate ends, and at a proper
  -- nonempty `E` the blocks are exactly `E` and `S \ E`.  `eventPartition_compl` records
  -- that `X_E` cannot tell `E` from its complement, which is why Definition 46's two clauses
  -- do not repeat each other; on `coordFS`, `X_E` at a block of a coordinate factor is that
  -- factor, which is what makes the Definition 46 instances computable from §3.3 and §4.3
  -- material already on the witness.
  Examples.eventPartition_empty Examples.eventPartition_univ
  Examples.eventPartition_classes Examples.eventPartition_compl
  Examples.eventPartition_vsnd Examples.eventPartition_vfst
  -- Definition 46 inhabited, and **both** clauses shown load-bearing at the two failure
  -- shapes the paper itself names.  The positive instance reads the first coordinate as the
  -- agent's action, "the second coordinate is `true`" as the event, and the second
  -- coordinate as the world model.  `not_observes_snd_vsnd_true` is the transparent-Newcomb
  -- shape (Drescher): the action *is* the event, so clause 1 fails for every world model.
  -- `not_observes_snd_snd_Efalse` is the counterfactual-mugging shape (Nesov): clause 1
  -- holds and clause 2 fails, because on the branch where the event fails the action still
  -- determines the whole world model.  Neither clause therefore implies the other.
  Examples.observes_fst_snd_vsnd_true Examples.not_observes_snd_vsnd_true
  Examples.not_observes_snd_snd_Efalse
  -- What `observes_fst_snd_vsnd_true` does *not* pin: at that `(W, E)` the complement is a
  -- block of `W`, so `W|Eᶜ` is indiscrete and clause 2 holds of **every** agent —
  -- `observes_snd_vsnd_true_iff` proves the collapse to clause 1 outright.  The witness
  -- with a substantive clause 2 is `observes_fst_snd_empty`: at `E = ∅` the complement is
  -- all of `S`, so clause 2 is the unconditional `fstFactor ⊥^F sndFactor` against a
  -- nonempty restricted history, and `not_observes_snd_snd_empty` is the matching failure.
  Examples.observes_snd_vsnd_true_iff Examples.observes_fst_snd_empty
  Examples.not_observes_snd_snd_empty
  -- Definition 47 inhabited at a two-block partition, with the constant family
  -- `A_x = fstFactor`, and tied to Definition 46 on an instance —
  -- `observes_and_observesPartition_vsnd_true` exhibits the same agent and world model
  -- observing the event `E` and the partition `X_E` — rather than by a general lemma, which
  -- the paper does not state either.  `observesPartition_top` is the corner that keeps the
  -- positive instance honest: `Ind_S` observes every partition with respect to every world
  -- model, so a Definition 47 witness says something only once its agent is nontrivial.
  -- A second honesty corner, disclosed rather than discharged by the two positive instances
  -- above: in both `observes_fst_snd_vsnd_true` and `observesPartition_fst_snd` the set the
  -- second clause conditions on is a *block* of the world model `W`, so `W|Eᶜ` is
  -- indiscrete, its history is empty, and clause 2 holds for **every** agent and every
  -- sub-agent family.  Those two therefore meter clause 1 and the inhabitation of
  -- Definition 47's `∃ As`, not the sub-agent decomposition.  A witness that meters clause 2
  -- needs `h^F(W|Eᶜ) ≠ ∅`, and a witness that meters the decomposition needs a
  -- *non-constant* family — at a constant family `sInf (Set.range As) = A` by
  -- `sInf_singleton`, so the `∃ As` does no work.
  Examples.classes_sndFactor Examples.observesPartition_fst_snd
  Examples.observes_and_observesPartition_vsnd_true Examples.not_observesPartition_snd
  Examples.observesPartition_top
  -- Both of those use a *constant* sub-agent family, where `⋁_S {Aᵢ} = A` is
  -- `sInf_singleton` and the decomposition does nothing; and at `W = X = sndFactor` clause
  -- 2 again collapses to clause 1 for every agent (`observesPartition_snd_snd_iff`).
  -- `observesPartition_fst_snd_nonconstant` is the instance where the family genuinely
  -- varies, with the non-constancy in the statement.  Its two values are comparable, and
  -- that is forced rather than lazy: clause 1 admits only `fstFactor` and `Ind_S` as agents
  -- for a two-block `X` on this carrier, and `Ind_S` is the only partition strictly coarser
  -- than a factor there — an incomparable family needs more than two factors.
  Examples.observesPartition_snd_snd_iff Examples.observesPartition_fst_snd_nonconstant
  -- Definitions 48-49 separated by the agreement partition ("do the two coordinates
  -- match?").  Definition 48 holds at a factor, at `Ind_S` and at `Dis_S`, and fails at the
  -- agreement partition for the paper's own reason: it is too coarse to specify the
  -- counterfactual, its history being the whole basis, so `⋁_S(h^F(X)) = Dis_S ≠ X`.
  -- Definition 49 is then implied by Definition 48 for every `W`
  -- (`FactoredSet.counterfactableRel_of_counterfactable`, general, in `EmbeddedAgency.lean`
  -- with the other §7.3 reductions), holds of the agreement partition relative to `Ind_S` —
  -- where `FactoredSet.counterfactableRel_top` shows the corner is general, so that instance
  -- alone would certify nothing — and *fails* of it relative to `fstFactor`, which is what
  -- makes Definition 49 neither empty nor total.
  Examples.counterfactable_fstFactor Examples.counterfactable_top
  Examples.counterfactable_bot Examples.not_counterfactable_xorPart
  Examples.counterfactableRel_fstFactor
  Examples.not_counterfactable_but_counterfactableRel_xorPart
  Examples.not_counterfactableRel_xorPart_fstFactor
  -- Definition 50 against Definition 19.  At `E = S` the two agree
  -- (`FactoredSet.beforeGivenSet_univ_iff`, general, in `EmbeddedAgency.lean`), and away
  -- from it they genuinely differ — the coordinate factors are incomparable in `≤^F`, yet on
  -- the diagonal each is before the other, which is the §7.3 shadow of §4.3's "restriction
  -- can entangle".  The negative and the two degenerate corners keep it from being read as
  -- total: given `∅` every pair is ordered, and `Ind_S` is before everything given anything.
  Examples.beforeGivenSet_fst_bot_univ
  Examples.beforeGivenSet_fst_snd_Ediag Examples.not_beforeGivenSet_fst_top_Ediag
  Examples.beforeGivenSet_corners
-- FFS-INVENTORY-END

/-! Tier-2 boundary structures for the Finite Factored Sets surface. -/
#assert_fields FiniteFactoredSets.IsFactorization
  nontrivial bijective
#assert_fields FiniteFactoredSets.FactoredSet
  B isFactorization
#assert_fields FiniteFactoredSets.Subpartition
  r symm' trans'
#assert_fields FiniteFactoredSets.ProbDist
  P nonneg empty univ additive
#assert_fields FiniteFactoredSets.Model
  S F f finite
#assert_fields FiniteFactoredSets.OrthDatabase
  O N

/-! ## Condensation (Eisenstat 2025) — endpoint inventory

Nodes are cited by printed number (`Paper node: \`Definition 3.1\``) read off the committed
text extraction `Condensation/notes/condensation-25-07.txt`; `scripts/check-condensation-nodes.py`
enforces validity, anchoring, and that every annotated declaration appears in one of the
two blocks below.  Status: **statements and proofs complete** as of M2 (landed
2026-08-18).  Every in-scope node of §2, §3, §3.1, §4 and §5 has a carrier, every carrier
is proved, and there is **no `sorry` anywhere in `Condensation/`**:
`scripts/check_sorry_ledger.py` enumerates every `sorryAx`-dependent declaration of the
library from the compiled environment and reports zero for this paper.  Consequently the
`CONDENSATION-PENDING` block below is **empty**, and the whole annotated surface is in the
`#assert_axioms_clean` block.  (Examples 5.1-5.3 carry no declaration; they are
illustrations rather than claims, and the coverage ruling that excludes them is on the
record as *proposed*, not settled — `scripts/check-condensation-nodes.py` therefore reports
39/42 rather than 42/42.)

This is **not** the same as the paper being `completed` in `scripts/papers.py`: that status
additionally requires a curated `Condensation/API.lean` boundary, client tests in
`APITests/`, a human read-through and a final fresh-context audit, none of which has
happened.  The roadmap is `Condensation/notes/roadmap.md`.  There are **no** residual
modeling substitutions: the
`dd:finite-range` narrowing was retired on 2026-08-17, and `Condensation.RVModel` is now
Definition 3.1 verbatim — a countable discrete probability space *with finite entropy*
(`ShannonInformation.FiniteEntropyMeasure`) carrying countable-discrete-range variables of
finite entropy.  See `Condensation/README.md`.

**Why there are two blocks: the staged inventory.**  This formalization reached the
paper's endpoints statement-first, and the second block is the mechanism that made that
honest.  A declaration may carry a `Paper node:` annotation because its *statement* is
final and is the paper's real endpoint, while its proof is still `sorry`.  Such a
declaration cannot be listed in `#assert_axioms_clean`: that command exists to catch
exactly a `sorryAx` dependency, and listing it would either fail the build or tempt someone
to weaken the check.  Dropping the `Paper node:` annotation instead would be a lie about
the statement's provenance, and the node checker would then also stop guarding the
statement.

**The pending block is empty by construction, and is retained deliberately.**  M2
discharged the last staged endpoint, so nothing is named there today.  It is kept, rather
than deleted, because it is a live gate in both directions: `check_sorry_ledger.py` fails
on a `sorryAx`-dependent declaration that is named in neither section *and* on a ledger
entry that no longer depends on `sorryAx`, so an empty block is an assertion that there is
nothing to stage, re-checked on every run.  Deleting it would remove the assertion, not
record it.  A future statement-first endpoint is staged by adding a line back.

So the annotated surface is split.  The `CONDENSATION-INVENTORY` block below is the
ordinary axiom gate.  The `CONDENSATION-PENDING` block that follows it is **pure Lean
comment** — it compiles to nothing and asserts nothing — and names, one per line with a
reason, every annotated endpoint that is not yet axiom-clean.  It is a declaration of
intent, not a discharge.

The pending block has **two sections**, separated by a `-- SECTION: …` marker line.  The
first names annotated endpoints.  The second, `consumers (un-annotated)`, names
declarations that depend on `sorryAx` but carry no `Paper node:` line at all — small
consequences of a staged theorem, which are not claims about the paper and so cannot be
annotated, but which a reader must still not mistake for proved.  Round 2 found three of
them living outside both blocks (R2-F22), which is precisely the drift the ledger exists to
prevent; `scripts/check_sorry_ledger.py` now enumerates every `sorryAx`-dependent
declaration of the library from the compiled environment and fails on any that is named in
neither section, so the two sections together are mechanically complete rather than
maintained by hand.

`scripts/check-condensation-nodes.py` (via the generic `pending_block` support in
`scripts/paper_nodes.py`, available to any paper) accepts an annotated declaration listed
in *either* block, and fences the staging with four hard failures: a name in both blocks,
a pending entry naming no annotated declaration (a stale entry outliving its endpoint), a
malformed pending line, and a non-empty pending block once `scripts/papers.py` registers
the paper `completed`.  A surviving non-empty block prints as a note carrying the count,
which is the number to watch shrink; it prints no such note now.  **Moving a name from the
pending block to the inventory block is what "M2 proved this endpoint" means**; the two
edits belong in the same commit as the proof, and M2 made the last of them. -/

-- CONDENSATION-INVENTORY-BEGIN
#assert_axioms_clean
  -- §2 conventions (Condensation/Probability.lean).  Definition 2.1 has three carriers:
  -- the Mathlib rendering `IsRandomVariable` and the "function of" conventions.
  Condensation.IsRandomVariable Condensation.FunctionOf Condensation.AEFunctionOf
  Condensation.AEFunctionOf.of_functionOf Condensation.AEFunctionOf.comp Condensation.AEFunctionOf.trans Condensation.AEFunctionOf.prodMk
  Condensation.AEFunctionOf.comp_measurePreserving Condensation.aeFunctionOf_self
  -- eq. (2.2): pullback invariance along probability-preserving maps.
  Condensation.identDistrib_comp_measurePreserving Condensation.entropy_comp_measurePreserving
  Condensation.mutualInfo_comp_measurePreserving Condensation.condEntropy_comp_measurePreserving
  Condensation.PPlus Condensation.PPlus.toFinset Condensation.PPlus.single Condensation.PPlus.le_iff Condensation.PPlus.lt_iff
  Condensation.interactionInfo Condensation.interactionInfo_comm Condensation.interactionInfo_swap Condensation.condInteractionInfo
  Condensation.GiryMeasurableSpace
  -- Proposition 2.5 (the determinism bridge), its converse and the iff, and the two
  -- entropy consequences §4 uses.
  Condensation.aeFunctionOf_of_condEntropy_eq_zero Condensation.condEntropy_eq_zero_of_aeFunctionOf
  Condensation.aeFunctionOf_iff_condEntropy_eq_zero Condensation.entropy_le_of_aeFunctionOf Condensation.entropy_pair_of_aeFunctionOf
  -- Definitions 3.1–3.4 (Condensation/Model.lean).
  Condensation.RVModel Condensation.RVModel.joint Condensation.RVModel.jointOn Condensation.RVModel.measurable_joint Condensation.RVModel.measurable_jointOn
  Condensation.contrib Condensation.above Condensation.strictAbove Condensation.contribIdx Condensation.mem_contrib_iff
  Condensation.contribIdx_eq_contrib_singleton Condensation.contribIdx_eq_above_singleton Condensation.strictAbove_subset_above
  Condensation.LatentModel Condensation.LatentModel.jointOn Condensation.LatentModel.jointContrib Condensation.LatentModel.jointAbove
  Condensation.LatentModel.jointStrictAbove Condensation.LatentModel.jointContribIdx Condensation.LatentModel.pullbackJoint
  Condensation.LatentModel.measurable_pullbackJoint
  Condensation.LatentModel.simpleScore Condensation.LatentModel.condScore Condensation.LatentModel.reconScore
  -- Non-vacuity witnesses (Condensation/Examples.lean): a constructed model and latent model.
  Condensation.coinModel Condensation.coinLatent Condensation.coinModel_entropy_pos Condensation.coinLatent_nonempty
  -- §3.1 (Condensation/Morphism.lean).  All ten endpoints of the section are proved:
  -- Definitions 3.5, 3.6, 3.9, 3.10 and Propositions 3.7, 3.8, 3.11, 3.12.  `RVModel.Hom`
  -- carries no measurability field for `f` -- Definition 3.5's own remark is that it is
  -- automatic on countable discrete ranges -- and the category laws (3.17)-(3.20) hold by
  -- `rfl`.  Definition 3.10 has two carriers, the pair predicate and the existential.
  Condensation.RVModel.Hom Condensation.RVModel.Hom.comp
  Condensation.RVModelObj.instCategory Condensation.RVModel.Hom.isIso_iff
  Condensation.RVModel.Hom.AEEq
  Condensation.RVModel.IsEquivalence Condensation.RVModel.Equivalent
  Condensation.RVModel.Hom.aeEq_equivalence Condensation.RVModel.Hom.comp_aeEq_congr
  Condensation.RVModelObj.equivalent_equivalence
  -- §4 (Condensation/Perfect.lean, Amalgamation.lean, Comparison.lean, Examples.lean).
  -- All three of Proposition 4.2's inequalities are here as of M2, including the middle
  -- one, (4.7)-(4.9), which used to be staged; Corollary 4.6, whose proof consumes it,
  -- came with it.  Definitions 4.11 and 4.12 are structures and are clean as such.
  --
  -- **Lemma 4.13 is complete as of 2026-08-17.**  Its three supporting measure lemmas --
  -- (4.55)-(4.56) total mass and both halves of (4.57) -- were the library's last
  -- un-annotated `sorry`s, and were discharged against Mathlib's
  -- `Measure.sum_smul_dirac_singleton` / `Measure.sum_smul_dirac` and the (4.53) weight
  -- rewritten as an indicator on `Λ₁ × Λ₂`.  All four of its carriers -- the two `canonical`
  -- constructions and the two existence statements -- are therefore inventoried here
  -- rather than staged, and every remaining `sorry` in the library now sits inside a
  -- declaration that carries a paper-node annotation.
  Condensation.LatentModel.simpleScore_ge_condScore
  Condensation.LatentModel.condScore_ge_entropy_jointContrib
  Condensation.LatentModel.entropy_jointContrib_ge_entropy_joint
  Condensation.LatentModel.PerfectlyCondenses Condensation.LatentModel.SimplyPerfectlyCondenses
  Condensation.LatentModel.perfect_entropy_iff_aeFunctionOf
  Condensation.LatentModel.aeFunctionOf_of_perfectlyCondenses
  Condensation.LatentModel.perfect_tfae_A Condensation.LatentModel.perfect_tfae_B
  Condensation.LatentModel.aeFunctionOf_iff_isEquivalence_contribModel
  Condensation.RVModel.OrderedMarkov Condensation.RVModel.orderedMarkov_iff
  Condensation.Amalgamation Condensation.LatentAmalgamation
  Condensation.Amalgamation.canonical Condensation.nonempty_amalgamation
  Condensation.LatentAmalgamation.canonical Condensation.nonempty_latentAmalgamation
  Condensation.Example41.L₁ Condensation.Example41.L₂
  Condensation.Example44.M44 Condensation.Example44.L44
  -- Example 4.1's (4.2)-(4.5) and Example 4.4's (4.11) and conclusion: proved at M2.
  Condensation.Example41.L₁_simpleScore Condensation.Example41.L₁_condScore
  Condensation.Example41.L₂_simpleScore Condensation.Example41.L₂_condScore
  Condensation.Example44.entropy_joint_eq Condensation.Example44.simplyPerfectlyCondenses
  -- §5 (Condensation/Quantitative.lean): Lemma 5.4 in both printed forms, Definition 5.5's
  -- polar, Definition 5.6's intersection tree with its computed labels and its family of
  -- intersections (5.11), Proposition 5.7 in full (existence and uniqueness of the
  -- extension of a leaf labelling), and Corollary 5.10's (5.24).  Theorem 5.8, Corollary
  -- 5.9 and Corollary 5.10's (5.25) were staged when this comment was first written; all
  -- three were **proved at M2** and are inventoried at the foot of this block, so the
  -- staged half of the §5 surface is now empty.
  --
  -- Proposition 5.7 is the **`M`-version** since 2026-08-17 (R2-F08/F11): the paper's `ℓ̃`
  -- maps the leaves *into an intersection-closed collection `M`* and the unique extension
  -- is a function `ℓ : V → M`, so `existsUnique_intersectionTree` now takes `M`, its
  -- closure under `⊓`, and `t.LabelsIn M`, and concludes with `d.LabelsIn M` as a third
  -- conjunct.  The earlier ambient-lattice statement is kept, un-annotated, as
  -- `existsUnique_intersectionTree_ambient` in the machinery block below; it is not
  -- Proposition 5.7.
  Condensation.condEntropy_eq_of_pair Condensation.condEntropy_le_of_pair
  Condensation.polar
  Condensation.ITree Condensation.ITree.label Condensation.ITree.intersections
  Condensation.ITree.LabelsIn
  Condensation.ITree.label_eq_leaves_foldr
  Condensation.eq_decorate_of_isIntersectionTree Condensation.existsUnique_intersectionTree
  Condensation.polar_kSubsets
  -- Lemma 4.14 (Comparison.lean), proved at M2 with the [MeasurableSingletonClass S] binder ruling.
  Condensation.aeFunctionOf_of_condIndepFun
  -- Theorem 4.15 (Comparison.lean), proved at M2 (the induction the paper omits — erratum 5 — is `aeFunctionOf_jointAbove_aux`).
  Condensation.aeFunctionOf_jointAbove_of_perfectlyCondenses
  -- M2: Theorem 5.8 in both printed forms, Corollary 5.9 (both forms) and Corollary 5.10's (5.25).
  Condensation.condEntropy_jointAbove_eq Condensation.condEntropy_jointAbove_le
  Condensation.condEntropy_jointAbove_le_reconScore
  Condensation.condEntropy_jointAbove_le_reconScore_of_orderedMarkov
  Condensation.condEntropy_jointAbove_le_choose
-- CONDENSATION-INVENTORY-END

-- The staged half of the Condensation annotated surface: endpoints whose *statements* are
-- final and carry a `Paper node:` line, but which are not yet axiom-clean -- either their
-- own proof is `sorry` or they consume one.  This block is pure comment; it compiles to
-- nothing and asserts nothing.  See the preamble above for the four failure modes
-- `scripts/check-condensation-nodes.py` fences it with.  Moving a name from here into the
-- `#assert_axioms_clean` block above is what "M2 proved this endpoint" means, and the two
-- edits belong in the same commit as the proof.
--
-- **Both sections are empty as of M2 (2026-08-18), and that is the point.**  There is no
-- `sorry` left in `Condensation/`, so there is nothing to stage.  Do not delete the block:
-- `scripts/check_sorry_ledger.py` cross-checks it against the compiled environment in both
-- directions on every run, so "empty" is a re-verified assertion rather than an absence.
-- The `-- SECTION:` marker line must stay for the same reason -- the second section is
-- where an un-annotated consumer of a staged theorem would be named (R2-F22).
--
-- CONDENSATION-PENDING-BEGIN
-- SECTION: consumers (un-annotated)
-- CONDENSATION-PENDING-END

/-! Tier-2 boundary structures for the Condensation surface.

Two things a reader should not mistake for omissions.  `RVModel`'s index type carries
`[Finite I]` — Definition 3.1's *finite* family — as a **class parameter of the structure**,
not as a field, so it is correctly absent from the freeze below; it has to be a parameter,
because `Finite I` does not mention the model and instance search would never find it as a
field (the concrete symptom was `reconScore` elaborating at `I = ℕ` with every sum silently
empty).  And `LatentModel`'s universes are independent of its model's — the full parameter
list is `LatentModel.{u, v, w, u', v'}` — which likewise changes no field. -/
#assert_fields Condensation.RVModel
  Ω mΩ countΩ singΩ P probP finiteEntropy_Ω R mR countR singR X measurable_X finiteEntropy_X
#assert_fields Condensation.LatentModel
  L π π_pres contributes

/-! The §3.1 and §4 boundary structures.

`RVModel.Hom` has **no measurability field for `f`**, and that absence is load-bearing
rather than an omission: Definition 3.5's own remark is that `f_j` is automatically
measurable because the ranges are countable and discrete, so a field would be a
strengthening of the paper's data.  `RVModel.Hom.measurable_f` supplies it as a lemma.
`RVModelObj` carries the index type `I` as a **field**, with `Finite I` as an instance
field beside it, because Definition 3.5 lets a morphism change the index set and a
`Category` instance needs a single object type — the opposite of `RVModel`, where the same
`Finite I` must be a *parameter*.  `IsEquivalence` is a `Prop`-valued structure, so
freezing its two fields freezes the two clauses of Definition 3.10.

`LatentAmalgamation`'s field list is long because Definition 4.12's "two latent variable
models with underlying probability space `Λ₀`" is rendered with `Λ₀` primary and the two
models *derived* (`lat₁`, `lat₂`), which is what makes their carrier `Λ₀` definitionally
rather than by a transported type equality.  Its last field, `comm`, is the **only** one
not read off Definition 4.12: nothing in the printed clause ties `π̃₁` to `π̃₂`, and Theorem
4.15 needs them to agree almost everywhere (`Condensation/notes/paper-errata.md` entry 10).

What the list no longer contains is the point of the 2026-08-17 freeze (R2-F12/F20).  Two
fields `ρ₁_π`/`ρ₂_π`, saying `Lₖ.π ∘ ρₖ = π̃ₖ` almost everywhere, were deleted: Definition
4.12(3)'s `ρₖ` are morphisms in the sense of **Definition 3.5**, i.e. of the underlying
*random variable* models, whose only conditions are "probability preserving" and
`fⱼ(X_{ι(j)}) = ρₖ^* Yⱼ` a.e.  The paper defines no morphism of *latent* variable models
and asks for no compatibility with the maps to `Ω`, so those fields were a strengthening of
the printed data.  What survives of clause (3) is exactly `ρₖ_pres` and `ρₖ_Y`.  A future
change that reintroduces either field is a faithfulness regression, and this freeze is what
catches it. -/
#assert_fields Condensation.RVModel.Hom
  π π_pres ι f eq_ae
#assert_fields Condensation.RVModelObj
  I finI M
#assert_fields Condensation.RVModel.IsEquivalence
  comp_left comp_right
#assert_fields Condensation.Amalgamation
  π₁_pres π₂_pres Λ₀ mΛ₀ countΛ₀ singΛ₀ P₀ probP₀ «ρ₁» «ρ₂» ρ₁_pres ρ₂_pres comm
#assert_fields Condensation.LatentAmalgamation
  Λ₀ mΛ₀ countΛ₀ singΛ₀ P₀ probP₀ finiteEntropy_Λ₀
  Y₁ measurable_Y₁ finiteEntropy_Y₁ «π₁» π₁_pres contributes₁
  Y₂ measurable_Y₂ finiteEntropy_Y₂ «π₂» π₂_pres contributes₂
  «ρ₁» ρ₁_pres ρ₁_Y «ρ₂» ρ₂_pres ρ₂_Y comm

/-! ## Factored Space Models — the checked endpoint inventory

Same contract as the FFS-INVENTORY block above: every declaration carrying a
`Paper node:` annotation in `FactoredSpaces/` must itself be listed between the
FS-INVENTORY markers below, and `scripts/check-factored-spaces-nodes.py` enforces that
direction, together with the validity of each cited node against the committed TeX
(`printed-counter-appendix` scheme: section-scoped shared counter, lettered appendix,
`restatable` wrappers) and the anchoring of each annotation to a named declaration.  The
converse (every listed name is a real declaration) is caught only when this file is
elaborated.

This formalization is **complete** (`scripts/papers.py`: `completed`): all 50 numbered
nodes of the paper are annotated and inventoried, and `notes/scope-manifest.json` records
that nothing was ruled out of scope.  Besides the numbered nodes the block carries three
kinds of unannotated entries, all deliberate: the non-vacuity witnesses of
`FactoredSpaces/Examples.lean`; the working form `disintegrates_iff_splice` of Definition
4.5 (the equivalence every history proof goes through, audited beside its definition); and
the claims the paper makes without a number —
`not_isGraphoid_structIndepRel` (Table 1, row "Intersection": structural independence
is *not* a graphoid; §5.1 calls this an important property) and
`isSemigraphoid_condIndepRel` (the Pearl 1988 fact cited in the proof of Proposition
5.2, proved here so that no citation boundary remains).  Neither can carry a
`Paper node:` line, since the checker admits only numbered nodes.
A third unnumbered entry joins them: `not_intersection_structIndepRel`, the same Table 1
"Intersection" claim with the failing axiom written out, so that reading the negative
claim needs no Proposition 5.2 alongside it. -/

open FactoredSpaces in
-- FS-INVENTORY-BEGIN
#assert_axioms_clean
  -- §4.1: Definitions 4.1, 4.2 and Lemma C.3
  Pt bg DerivedOn derivedOn_iff
  -- §4.2 / Appendix A: Definitions 4.5, 4.6; Lemmas 4.7, 4.8, 4.9, A.1, A.2, C.4
  Disintegrates disintegrates_iff_splice Disintegrates.union Disintegrates.inter
  Generates history generates_history history_subset_of_generates history_unique_minimal
  Generates.inter history_pair history_eq_iUnion_fibers history_eq_biUnion_fibers
  generates_indic_iff_agree generates_indic_iff_splice eventHistory_minimal_splice
  -- §4.3–4.4 / Appendix B: Definitions 4.10, 4.11; Lemmas 4.12, B.1
  StructIndep StructIndepGiven Before StrictlyBefore
  structIndep_of_before before_of_forall_bg before_iff_forall_structIndep
  structIndepGiven_pair
  -- Probability substrate: Definitions 4.3, 4.4, 6.1, C.1, C.2; Lemmas C.11, C.13, C.14,
  -- C.15, C.16, C.17
  Factorizes IsFactoredSpaceModel Distr.marg Distr.outer
  Distr.prob_pos_of_support_subset Distr.support_outerCompl Distr.prob_pos_of_marg_support_subset
  CondIndep CondIndepVar CondIndepEventVar.of_pair CondIndepEventVar.of_proj_subset
  Distr.prob_cyl_inter_cyl Factorizes.prob_sliceAt Distr.prob_outerCompl_delta
  condIndepVarEvent_proj_history
  -- §6 / Appendix C.2–C.3: Lemmas 6.3, 6.4, 6.5, C.5, C.7, C.8, C.9, C.10, C.12, C.18,
  -- C.19, C.20; Definition C.6; Theorem 6.2; Proposition 6.6
  condIndep_of_disjoint_eventHistory
  exists_polynomial_interp_prob interp_prob_pos condIndepVar_of_local
  interp_mem_factorizingPos
  PQIrrelevant Irrelevant cohistory pqIrrelevant_or_of_condIndepAll
  cohistory_union_eq_univ_of_condIndepAll condProb_eq_of_agree_on_relevant
  condIndepEventVar_proj_cohistory condIndepVarEvent_proj_cohistory disintegrates_cohistory
  cohistory_eq_compl_eventHistory disjoint_eventHistory_of_condIndepAll
  structIndepGiven_iff_forall_condIndepVar structIndepGiven_iff_forall_condIndepVar_of_nonempty
  structIndepGiven_of_open
  -- §5.1: Definition 5.1, Proposition 5.2; plus the two unnumbered claims named in the
  -- preamble (Table 1 "Intersection" row; the Pearl semigraphoid fact behind Prop 5.2)
  IsSemigraphoid IsGraphoid IsCompositionalSemigraphoid
  isCompositionalSemigraphoid_structIndepRel not_isGraphoid_structIndepRel
  not_intersection_structIndepRel
  isSemigraphoid_condIndepRel
  -- §5.2 / Appendix B: Lemma 5.3, B.2; Propositions 5.4, 5.5, 5.6, 5.8; Definition 5.7
  prob_jointVar_fiber factorizesOverDAG_tau factorizes_tauInv tau_tauInv tauPos_bijective
  tauInv_condCPD_tau
  factorizesOverDAG_iff_isFactoredSpaceModel isAncestor_iff_strictlyBefore
  dSeparated_iff_structIndepGiven
  IsPerfectMapDAG IsPerfectMapFSM isPerfectMapFSM_nodeVar_of_isPerfectMapDAG
  exists_isPerfectMapFSM_of_exists_isPerfectMapDAG exists_isPerfectMapFSM_not_exists_isPerfectMapDAG
  -- Non-vacuity witnesses and convention pins (`FactoredSpaces/Examples.lean`): the paper's
  -- two-coin example, the trivial one-factor model of every distribution (remark after
  -- Definition 4.4), the collider DAG pinning the `dd:dsep` conventions from both sides
  -- (`not_dSeparated_self_zero` and `dSeparated_given_endpoint` are the two discriminating
  -- endpoint pins), Props 5.5/5.6 with content — `StructIndepGiven` positively inhabited
  -- (`structIndepGiven_collider`) as well as refuted — and the first inhabitant of
  -- `IsPerfectMapDAG` (Prop 5.8(1) is not vacuous).
  Examples.disintegrates_univ_diag Examples.not_disintegrates_singleton_diag
  Examples.history_bg_zero Examples.structIndep_bg_zero_one Examples.not_structIndep_bg_self
  Examples.isFactoredSpaceModel_single
  Examples.collider_isAcyclic Examples.not_dSeparated_given_collider
  Examples.not_colliderTrail_active_empty Examples.dSeparated_parents_of_collider
  Examples.nil_active_zero Examples.not_nil_active_zero Examples.not_dSeparated_self_zero
  Examples.not_dSeparated_adj Examples.dSeparated_given_endpoint
  Examples.structIndepGiven_collider Examples.not_structIndepGiven_nodesVar
  Examples.strictlyBefore_nodeVar Examples.G₁_acyclic Examples.isPerfectMapDAG_G₁_Q
  -- Negative instances of the paper's three *factorizes* predicates, so that none of them
  -- is trivially true: a constant observation variable is not a factored space model of a
  -- non-degenerate law (Definition 4.4), and the perfectly-correlated two-coin law `Pdiag`
  -- factorizes neither over `Ω` (Definition 4.3) nor over the edgeless two-node DAG `G₀`
  -- (§5.2, eq. (2)).
  Examples.not_isFactoredSpaceModel_const
  Examples.not_factorizes_diag
  Examples.G₀_acyclic
  Examples.not_factorizesOverDAG_diag
  -- Definition 5.7(1) inhabited by a DAG that actually has an edge, so that neither side
  -- of its equivalence is idle: `G₂ = (0 -> 1)` is a perfect map of the law `Pedge` whose
  -- two coordinates are dependent.  `not_dSeparated_G₂` / `dSeparated_G₂_given_endpoint`
  -- pin the graph side and `not_condIndepVar_Pedge` the probability side.
  Examples.G₂_acyclic
  Examples.G₂_adj_zero_one
  Examples.not_dSeparated_G₂
  Examples.dSeparated_G₂_given_endpoint
  Examples.not_condIndepVar_Pedge
  Examples.isPerfectMapDAG_G₂_Pedge
  -- The empty-value-space errata (E12, E16), kernel-checked rather than asserted in prose
  Examples.generates_not_inter_closed_twoEmpty Examples.history_ne_iUnion_fibers_oneEmpty
  Examples.history_bg_eq_empty_twoUnit
-- FS-INVENTORY-END

/-! Tier-2 boundary structures for the Factored Space Models surface. -/
#assert_fields FactoredSpaces.Distr
  mass nonneg sum_eq_one
-- `#assert_fields` freezes field *names* only.  The content of these three structures is
-- carried by the field *types*: `IsGraphoid.intersection` carries the cross-typed side
-- condition `β = γ → ¬ HEq Y Z` (the paper's `Y ≠ Z`), and the `[Nonempty _]` binders on
-- the axiom fields are the minimal ones Theorem 6.2 needs — weakening either would pass
-- this freeze silently, so any such change must be reviewed against
-- `FactoredSpaces/KNOWLEDGE.md` (round-1 record) rather than trusted to the audit.
#assert_fields FactoredSpaces.IsSemigraphoid
  symm decomposition weakUnion contraction
#assert_fields FactoredSpaces.IsGraphoid
  toIsSemigraphoid intersection
#assert_fields FactoredSpaces.IsCompositionalSemigraphoid
  toIsSemigraphoid composition
#assert_fields Digraph.Trail
  verts chain head last nodup
#assert_fields Digraph.Walk
  verts chain head last

/-! ## Consumer API conveniences (not paper endpoint inventories)

The trust-surface inventories above remain the paper-facing accounting.  These
declarations instead belong to the supported consumer surface: they are small
extensionality, simplification, certification, and transport tools advertised in each
paper's consumer API module, a subset of which is exercised by `APITests`.
Axiom-checking them here does not designate them as paper claims or add them to any
`*-INVENTORY` block. -/

open LogicalInduction in
#assert_axioms_clean
  DeductiveProcess.ext Strategy.ext Trader.ext AffineCombination.ext LUV.ext
  RpnSentenceCodes.const

#assert_axioms_clean
  ModalAgent.formula_mkRank0 ModalAgent.arity_mkRank0 ModalAgent.rank_mkRank0
  BehavEquiv.outcome_congr BehavEquiv.cooperates_iff BehavEquiv.defects_iff
  BehavEquiv.provablyDefects_iff

open CartesianFrames in
#assert_axioms_clean
  Frame.Subagent.congr Frame.multSubagent_iff_multSubagentCategorical
  Frame.commit_outcome Frame.assume_outcome Frame.external_outcome
  Frame.externalQuot_outcome Frame.internal_outcome Frame.internalSect_outcome

-- Finite Factored Sets: the consumer-surface conveniences advertised in
-- `FiniteFactoredSets/API.lean`; a subset of them is exercised by `APITests`.
open FiniteFactoredSets in
#assert_axioms_clean
  FactoredSet.StrictlyBefore.before FactoredSet.strictlyBefore_def FactoredSet.before_def
  FactoredSet.orthogonal_def FactoredSet.orthogonal_iff_forall_notMem
  FactoredSet.entangled_iff FactoredSet.size_eq_mk FactoredSet.dim_eq_mk
  FactoredSet.dim_eq_zero_iff FactoredSet.generates_iff_rel
  FactoredSet.generates_iff_sInf_le FactoredSet.generates_iff_history_subset
  FactoredSet.le_iff_history_subset
  FactoredSet.chimera_self FactoredSet.chimera_sdiff FactoredSet.chimera_union
  FactoredSet.chimera_inter FactoredSet.chimera_left_idem FactoredSet.chimera_right_idem
  FactoredSet.chimera_left_comm FactoredSet.chimera_basis FactoredSet.chimera_empty
  -- The setwise companions of those projections, which §3-§5 quantify over:
  -- `mem_chimeraImage_self` is clause 3 read setwise, `chimeraImage_univ_univ` its
  -- specialization at `T = R = S`, and `chimeraImage_sdiff` is clause 4 read setwise.
  FactoredSet.mem_chimeraImage_self FactoredSet.chimeraImage_univ_univ
  FactoredSet.chimeraImage_sdiff
  Subpartition.ofSetoidOn Subpartition.dom_ofSetoidOn Subpartition.toSetoid_ofSetoidOn
  Subpartition.restrict_univ Subpartition.restrict_restrict_of_subset
  Subpartition.dom_restrict_ofSetoid Subpartition.part_restrict_ofSetoid
  Subpartition.restrict_ofSetoid_inf
  Subpartition.restrict_inter_subset_restrict_inf classes_top
  FactoredSet.generatesSub_iff_historySub_subset
  FactoredSet.orthogonalSub_def FactoredSet.beforeSub_def
  FactoredSet.strictlyBeforeSub_def FactoredSet.StrictlyBeforeSub.beforeSub
  FactoredSet.orthogonalSub_iff_forall_notMem FactoredSet.orthogonalSub_ofSetoid
  FactoredSet.beforeSub_ofSetoid FactoredSet.orthogonalGivenSet_def
  FactoredSet.orthogonalGiven_def FactoredSet.historySub_restrict_inf
  -- Definition 24 agrees with Definition 17 on a partition of `S` with no finiteness at
  -- all (`historySub_ofSetoid`: two `⋂₀`s over the same family), which is what lets
  -- Proposition 24, the two `*_ofSetoid` identifications above and
  -- `beforeGivenSet_univ_iff` below drop `[Finite F.B]`; Proposition 22's *least*-element
  -- sentence still needs it.  The two empty-history
  -- computations and the Definition 26 corners are the §4.3/§7.3 facts every consumer
  -- needs and no paper node states — `orthogonalGiven_given_self` in particular is NOT
  -- Proposition 25 (which covers only `W = X`) and is the mechanism behind Definition 48
  -- implying Definition 49.
  FactoredSet.historySub_ofSetoid
  FactoredSet.historySub_top_restrict FactoredSet.historySub_restrict_empty
  FactoredSet.historySub_restrict_eq_empty_iff
  FactoredSet.orthogonalGivenSet_comm FactoredSet.orthogonalGivenSet_top_left
  FactoredSet.orthogonalGivenSet_top_right FactoredSet.orthogonalGiven_given_self
  -- §2.1: Definition 8's second sentence, the binary common refinement.  The set form
  -- `commonRefinement` is the node; `commonRefinement_pair` is the bridge saying that the
  -- `⊓` in which Propositions 11, 13, 15 and 18 are stated *is* the paper's `X ∨_S Y`.
  commonRefinement_pair
  -- §7.3: the four reductions a client applies before reading a Definition 48-50 fact as
  -- §7 content rather than §3/§4 content.  `beforeGivenSet_univ_iff` is Definition 50 at
  -- `E = S` being Definition 19; the two `*_top`/`_empty` corners are vacuously total and
  -- are listed so a positive witness at them is not mistaken for content.  No paper node:
  -- §7 states no theorem about Definitions 46-50.
  FactoredSet.counterfactableRel_of_counterfactable FactoredSet.counterfactableRel_top
  FactoredSet.beforeGivenSet_univ_iff FactoredSet.beforeGivenSet_empty
  -- §5.1-§5.2: the polynomial surface.  `Q_eq_finsum_mono`, `Q_eq_sum`,
  -- `poly_eq_sum_image`, `mono_eq_prod`, `mono_congr`, `mono_union` and `poly_empty` are
  -- the unfoldings of Definitions 31-34; `coeff_poly`, `mem_support_poly`, `poly_ne_zero`
  -- and `monos_eq_of_support_eq` describe `poly^F_C(E)` monomial by monomial; and
  -- `mono_eq_iff`, `degreeOf_poly_le`, `mem_vars_poly`, `degreeOf_Q_le`, `Q_ne_zero`,
  -- `vars_disjoint_of_mul_eq_Q` are the squarefreeness facts Corollary 1 buys, with
  -- `mono_basis_injective` the separation of distinct elements underneath Proposition 26
  -- and `coeff_add_mul_of_split` the generic, upstreamable one.  `mem_irr` and
  -- `poly_dvd_Q` are §5.2's unfolding and divisibility corollary; `irr_isPartition`
  -- restates Proposition 29 in §4's vocabulary; `subset_chimeraImage_self` and
  -- `mem_iff_part_mem_vars` are the two §5.2 helpers §5.3 also runs on.  None of these is
  -- a paper node.
  FactoredSet.Q_eq_finsum_mono FactoredSet.Q_eq_sum poly_eq_sum_image
  mono_eq_prod mono_congr mono_union poly_empty
  coeff_poly mem_support_poly poly_ne_zero monos_eq_of_support_eq
  FactoredSet.mono_eq_iff FactoredSet.degreeOf_poly_le FactoredSet.mem_vars_poly
  FactoredSet.degreeOf_Q_le FactoredSet.Q_ne_zero FactoredSet.vars_disjoint_of_mul_eq_Q
  FactoredSet.mono_basis_injective coeff_add_mul_of_split
  FactoredSet.mem_irr FactoredSet.poly_dvd_Q FactoredSet.irr_isPartition
  FactoredSet.subset_chimeraImage_self FactoredSet.mem_iff_part_mem_vars
  -- §5.3: the two directions of Lemma 3 isolated from its `TFAE`, which is how §5.5 and a
  -- downstream client consume it.  Neither is a paper node of its own — the node is
  -- `orthogonalGiven_tfae`, inventoried above, and each of these is one of its projections.
  -- `eq_of_Q_eq` is the injectivity of `E ↦ Q^F_E` the `2 → 1` direction runs on.
  FactoredSet.Q_mul_Q_eq_of_orthogonalGiven FactoredSet.orthogonalGiven_of_Q_mul_Q_eq
  FactoredSet.eq_of_Q_eq
  -- §5.4: `ProbDist` is finitely additive, so a distribution is determined by its
  -- singletons on any finite set; these are the two forms of that, and they carry no
  -- finiteness of their own.  `diracAt` is the point mass, and `isDistribution_diracAt`
  -- is the general non-vacuity fact behind §5.4-§5.5: it is a distribution on *every*
  -- factored set of finite dimension, so the family Proposition 32 and Theorem 3 quantify
  -- over is empty only over an empty `S` — where Theorem 3's other side holds too.
  -- None of these is a paper node.
  ProbDist.eq_sum_singleton ProbDist.eq_sum_singleton_of_finite
  ProbDist.diracAt ProbDist.diracAt_apply FactoredSet.isDistribution_diracAt
  -- §6.1: Definition 39's third clause named for legibility.  The node itself is rendered
  -- by Mathlib — `f⁻¹(ω)` and `f⁻¹(E)` are `Set.preimage` and `f⁻¹(X)` is `Setoid.comap` —
  -- so `Model.pullback` carries no paper-node annotation and belongs here rather than in
  -- the inventory above; `pullback_apply` is its unfolding, which is how a client reads a
  -- Definition 42 or 45 statement pointwise.  `not_strictlyBefore_self_of_consistent` and
  -- `strictlyBefore_of_not_consistent` are the two ways a client reads Definition 45 before
  -- trusting it: irreflexive wherever `D` has a model, vacuously total where it has none.
  -- Neither is a paper node; the paper's positive instances are Propositions 34 and 36.
  Model.pullback Model.pullback_apply
  OrthDatabase.not_strictlyBefore_self_of_consistent OrthDatabase.strictlyBefore_of_not_consistent

-- Condensation: the consumer-surface conveniences of the M0 layer, and the constructed
-- non-vacuity witnesses added in the round-1 fix wave.  None of these carries a
-- `Paper node:` annotation and none belongs in the CONDENSATION-INVENTORY block above:
-- the instances and `famFinset`/`AEFunctionOf.pi`/`condEntropy_eq_entropy_of_subsingleton`
-- are plumbing a client needs but the paper never states, and the witnesses are what makes
-- Definitions 3.1-3.3 non-vacuous rather than statements *of* the paper.  (The two earlier
-- witnesses `coinModel`/`coinLatent` remain in the inventory block above, where they were
-- first listed.)  Two of the witness facts exist to correct a specific over-claim:
-- `coinLatent_reconScore` and `twoCoinLatent_reconScore` prove the reconstruction score is
-- *zero* on the easy witnesses -- perfect reconstruction is exactly what a vanishing
-- `ϱ_L` means -- and `noisyLatent_reconScore_pos` is the witness that it is not identically
-- zero.
open Condensation in
#assert_axioms_clean
  Condensation.instFiniteFinset Condensation.PPlus.instFinite
  Condensation.AEFunctionOf.pi Condensation.condEntropy_eq_entropy_of_subsingleton
  Condensation.RVModel.finiteEntropyOf
  Condensation.RVModel.finiteEntropy_joint Condensation.RVModel.finiteEntropy_jointOn
  Condensation.LatentModel.finiteEntropy_pullbackJoint
  Condensation.famFinset Condensation.mem_famFinset
  Condensation.RVModel.jointFamily Condensation.LatentModel.ofJoint
  Condensation.LatentModel.nonempty
  Condensation.coinLatent_reconScore
  Condensation.twoCoinModel Condensation.twoCoinLatent Condensation.twoCoin_famFinset_contrib
  Condensation.twoCoinLatent_simpleScore Condensation.twoCoinLatent_condScore
  Condensation.twoCoinLatent_condScore_lt_simpleScore Condensation.twoCoinLatent_reconScore
  Condensation.noisyModel Condensation.noisyLatent Condensation.noisyLatent_reconScore
  Condensation.noisyLatent_reconScore_pos Condensation.noisyLatent_simpleScore
  Condensation.noisyLatent_condScore
  -- Round 3 (2026-08-18): witnesses for the *conditions* of §4 rather than its structures
  -- (R3-F08).  Definitions 4.3 and 4.8 had no constructed inhabitant before this, so
  -- Theorem 4.9, Proposition 4.10 and Theorem 4.15 were non-vacuous only in the sense that
  -- their statements elaborate.  `coinLatent_perfectlyCondenses` is Definition 4.3's
  -- conditioned clause on the fair coin; `coinLatent_orderedMarkov` is Definition 4.8, got
  -- from it by Theorem 4.9's (B1 => B2) rather than proved by hand;
  -- `Example44.L44_coin_simplyPerfectlyCondenses` is the simple clause, and is also what
  -- discharges `Example44.simplyPerfectlyCondenses`'s joint-independence hypothesis on a
  -- constructed family (Mathlib's `ProbabilityTheory.iIndepFun.of_subsingleton` over the
  -- one-element `P⁺Unit`).
  -- `noisyLatent_not_perfectlyCondenses` is the NEGATIVE witness: perfect condensation is a
  -- real restriction, not a property every latent variable model has.  None of these is a
  -- paper statement -- the paper asserts no instance of Definition 4.3 beyond Example 4.4,
  -- which is `Example44.simplyPerfectlyCondenses` in the inventory block above -- so they
  -- belong here.
  --
  -- **The `coinLatent_*` witnesses above are DEGENERATE, and round 4 (R4-F23) corrected the
  -- over-claim this comment used to make.**  At `I = Unit` the ordered Markov condition
  -- holds for *every* `RVModel (PPlus Unit)` and `condScore = simpleScore` for *every*
  -- latent over an `RVModel Unit`, so `coinLatent_orderedMarkov` witnesses satisfiability
  -- and nothing about the content of Definition 4.8.  The witnesses that carry content are
  -- the `twoCoinLatent_*` ones at `I = Bool` listed further down, where `P⁺Bool` has three
  -- elements and `incomparable twoCoinT` is nonempty.
  Condensation.coinLatent_entropy Condensation.coinLatent_condScore
  Condensation.coinLatent_perfectlyCondenses Condensation.coinLatent_orderedMarkov
  Condensation.coinLatentRV_iIndepFun
  Condensation.Example44.L44_coin_simplyPerfectlyCondenses
  Condensation.Example44.L44_coin_perfectlyCondenses
  Condensation.noisyModel_entropy_joint Condensation.noisyLatent_not_perfectlyCondenses
  -- Round 4 (2026-08-18, R4-F23): the witnesses that carry CONTENT, at `I = Bool`, plus the
  -- two lemmas that prove the `Unit`-indexed ones above do not.
  --
  -- The degeneracy, proved rather than asserted: over a subsingleton `P⁺I`,
  -- `condScore_eq_simpleScore_of_subsingleton_index` says `χ_L = σ_L` for **every** latent
  -- variable model, and `incomparable_eq_empty_of_subsingleton_index` says Definition 4.8's
  -- family of incomparable indices is empty.  So at `I = Unit` neither Definition 4.3's
  -- distinction nor Definition 4.8's conditional independence has any content, and the
  -- `coinLatent_*` witnesses establish satisfiability only.
  --
  -- At `I = Bool` with all three latents equal to one fair coin: `χ_L = log 2` at each of
  -- the three nonempty `A` while `σ_L({true}) = 2 log 2`, so
  -- `twoCoinLatent_perfectlyCondenses` and `twoCoinLatent_not_simplyPerfectlyCondenses`
  -- **separate Definition 4.3's two clauses on a single witness** —
  -- `LatentModel.PerfectlyCondenses.of_simply` has no converse, and that is not observable
  -- at `I = Unit`.  `twoCoinLatent_orderedMarkov` inhabits Definition 4.8 where the
  -- condition is not vacuous: `twoCoin_incomparable_T` computes
  -- `incomparable twoCoinT = {twoCoinF}`, which is nonempty.
  Condensation.twoCoinF Condensation.twoCoinF_ne_twoCoinTF
  Condensation.condScore_eq_simpleScore_of_subsingleton_index
  Condensation.incomparable_eq_empty_of_subsingleton_index
  Condensation.twoCoin_famFinset_contrib_F Condensation.twoCoin_famFinset_contrib_TF
  Condensation.twoCoinLatent_condEntropy_F
  Condensation.twoCoinLatent_condScore_F Condensation.twoCoinLatent_condScore_TF
  Condensation.twoCoinLatent_perfectlyCondenses
  Condensation.twoCoinLatent_not_simplyPerfectlyCondenses
  Condensation.twoCoin_incomparable_T Condensation.twoCoinLatent_orderedMarkov
  -- Phase 4b (2026-08-17): the witness with an **infinite-range** variable, which the
  -- retired `dd:finite-range` narrowing excluded and Definition 3.1 admits.  `Ω = ℕ` under
  -- the geometric law of `ShannonInformation/FiniteEntropy/Examples.lean`, `X () = id`.
  -- `geomModel_not_finiteRange` is what makes the retirement demonstrably more than a
  -- re-spelling; `geomModel_entropy` rules out the degenerate reading in which the class
  -- grew only by variables of zero entropy.
  Condensation.Example.geomModel Condensation.Example.geomModel_X
  Condensation.Example.geomModel_P Condensation.Example.geomModel_not_finiteRange
  Condensation.Example.geomModel_entropy Condensation.Example.geomModel_entropy_pos
  Condensation.Example.geomLatent Condensation.Example.geomLatent_reconScore
  -- M1 additions, none of which carries a `Paper node:` annotation.
  --
  -- `Model.lean`: the generic joint-variable and index-family companions of
  -- `measurable_joint(On)` / `finiteEntropy_joint(On)` that §4 and §5 run on.  `jointAll` is
  -- `X_A` at `A = I` spelled as the dependent product over `I` itself, so that naming
  -- `X_I` in a statement needs only `[Finite I]` and not a `Fintype` datum to write
  -- `Finset.univ`; equations (4.4)-(4.5) of Example 4.1 use it for exactly that.
  -- `incomparable` is the auxiliary index family of Definition 4.8, beside
  -- `contrib`/`above`/`strictAbove`/`contribIdx` and carrying no node for the same reason.
  -- `isUpperSet_contrib`/`isUpperSet_above` are stated with Mathlib's `IsUpperSet` -- the
  -- library defines no synonym for "upward closed" -- and `contrib_injective` is what makes
  -- Theorem 5.8's leaf-bijection hypothesis equivalent to the multiset equation it is
  -- stated as.
  Condensation.RVModel.jointAll Condensation.RVModel.measurable_jointAll
  Condensation.RVModel.finiteEntropy_jointAll
  Condensation.RVModel.functionOf_jointOn_mono Condensation.RVModel.aeFunctionOf_jointOn_mono
  Condensation.RVModel.functionOf_joint Condensation.RVModel.entropy_joint_singleton
  Condensation.LatentModel.entropy_pullbackJoint
  Condensation.contribIdx_subset_contrib Condensation.incomparable
  Condensation.isUpperSet_contrib Condensation.isUpperSet_above Condensation.contrib_injective
  -- The five membership `Iff`s of the Definition 3.4 auxiliaries and of `incomparable`.
  -- They are `@[simp]` and mostly `Iff.rfl`, which is exactly why they were missed until
  -- R4-F27: a client rewrites with them constantly, so they are part of the supported
  -- boundary even though nothing here has to be *proved*.
  Condensation.mem_contrib Condensation.mem_above Condensation.mem_strictAbove
  Condensation.mem_contribIdx Condensation.mem_incomparable
  -- M2 additions.  `ChainRule.lean`: the chain rule for a *finite family* of joint
  -- variables along a strict linear order, which PFR does not have (it stops at the two-
  -- and three-variable forms) and which all four remaining §4 endpoints run on.  None of
  -- it is a numbered node: `entropy_jointOn_eq_sum` is the shape of (4.9)/(4.29)/(4.34),
  -- `condEntropy_jointOn_eq_sum` the shape of (4.38), `condEntropy_jointOn_mono` is (4.8),
  -- and the two `condIndepFun` bridges are the termwise equalities (4.30)/(4.35)/(4.40).
  -- The two order constructions are the paper's own linear extensions -- of reverse
  -- inclusion (4.7), and of the partial order `⪯ₚ` of the paragraph before (4.29).
  Condensation.exists_strictTotalOrder_ext
  Condensation.exists_revIncl_strictTotalOrder
  Condensation.exists_revIncl_strictTotalOrder_incomparable_first
  Condensation.pred_subset_incomparable_union_strictAbove
  Condensation.RVModel.condEntropy_pair_jointOn Condensation.RVModel.condEntropy_jointOn_mono
  Condensation.RVModel.condEntropy_jointOn_sdiff Condensation.RVModel.condEntropy_jointOn_above
  Condensation.RVModel.condEntropy_jointOn_eq_sum Condensation.RVModel.entropy_jointOn_eq_sum
  Condensation.RVModel.condEntropy_jointOn_eq_of_condIndepFun
  Condensation.RVModel.condIndepFun_of_condEntropy_jointOn_eq
  -- and the two directions of "joint independence of a finite family ⟺ additivity of
  -- entropy", which Theorem 4.9's (A1) ⟺ (A3) needs both of.  PFR's
  -- `iIndepFun.entropy_eq_add` is the forward direction only, and only at `Fin m`.
  Condensation.RVModel.entropy_jointOn_le_sum
  Condensation.RVModel.entropy_jointOn_eq_sum_of_iIndepFun
  Condensation.RVModel.entropy_jointOn_eq_sum_of_subset
  Condensation.RVModel.indepFun_X_jointOn_of_entropy_eq
  Condensation.RVModel.iIndepFun_of_entropy_jointOn_eq_sum
  -- The three consequences of Proposition 4.2's chain that used to sit in the pending
  -- block's `consumers` section: with (4.7)-(4.9) proved they are axiom-clean, and they
  -- are consequences of the chain rather than nodes of the paper, so they belong here.
  Condensation.LatentModel.entropy_joint_le_condScore
  Condensation.LatentModel.entropy_joint_le_simpleScore
  Condensation.LatentModel.PerfectlyCondenses.of_simply
  -- `Morphism.lean`: the §3.1 machinery around the endpoints.  `Hom.ofSameIndex` and
  -- `isEquivalence_ofSameIndex_iff` are the "laid out" characterization the paragraph after
  -- Definition 3.10 gives, which is the shape Proposition 4.7 consumes; `Hom.ext` needs
  -- `HEq` on the `f` component because `f`'s type mentions `ι`.
  Condensation.RVModelObj Condensation.RVModel.Hom.id
  Condensation.RVModel.Hom.measurable_f Condensation.RVModel.Hom.pullback_eq
  Condensation.RVModel.Hom.aeFunctionOf Condensation.RVModel.Hom.eq_ae_all
  Condensation.RVModel.Hom.ext
  Condensation.RVModel.Hom.IsMeasurableIso Condensation.RVModel.Hom.isMeasurableIso_of_bijective
  Condensation.RVModel.Hom.ofSameIndex Condensation.RVModel.isEquivalence_ofSameIndex_iff
  -- Definition 3.9 packaged as a `Setoid` on each hom-type (`dd:category`); the `≈`
  -- notation a client uses for a.e. equality of morphisms resolves through it (R4-F27).
  Condensation.RVModel.Hom.instSetoid
  Condensation.RVModel.Equivalent.refl Condensation.RVModel.Equivalent.symm
  Condensation.RVModel.Equivalent.trans
  Condensation.RVModelObj.Equivalent Condensation.RVModelObj.id_eq Condensation.RVModelObj.comp_eq
  -- `Perfect.lean`: the two random variable models Proposition 4.7 compares.  They are the
  -- objects the `↔` is *about*, and the `↔` is the node, so they carry no annotation of
  -- their own.
  Condensation.LatentModel.pullbackModel Condensation.LatentModel.contribModel
  Condensation.LatentModel.aeFunctionOf_jointContrib_pullbackJoint
  -- `Amalgamation.lean`: the derived halves of Definition 4.12, and the constructed
  -- non-vacuity witness.  `lat₁`/`lat₂` are the two latent variable models the definition
  -- names; their underlying space is `Λ₀` definitionally, which is what Theorem 4.15 needs.
  -- `diagonal` amalgamates a latent variable model with itself along the identity: it is
  -- the *axiom-clean* inhabitant of `LatentAmalgamation`, and therefore what makes Theorem
  -- 4.15 and every §5 statement non-vacuous today.  Lemma 4.13's `canonical` /
  -- `nonempty_latentAmalgamation` are the paper's own, stronger, existence claim; they were
  -- staged when this comment was written and were **proved on 2026-08-17**, so they now sit
  -- in the CONDENSATION-INVENTORY block above and are axiom-clean like everything else
  -- there.  The reason `diagonal` is still named as *the* non-vacuity witness is not that
  -- the others are unproved but that it is the one an existence-free argument may cite:
  -- a non-vacuity claim about Definition 4.12 must not be routed through Lemma 4.13's
  -- existence theorem (R2-F19).
  -- (The lemma `comm_ρ` stood here until 2026-08-17.  It said the square (4.43) commutes
  -- a.e. inside Definition 4.12, and was provable only from the fields `ρ₁_π`/`ρ₂_π`, which
  -- are not in Definition 4.12 and were deleted with it -- R2-F12/F20.)
  Condensation.LatentAmalgamation.rv₁ Condensation.LatentAmalgamation.rv₂
  Condensation.LatentAmalgamation.lat₁ Condensation.LatentAmalgamation.lat₂
  Condensation.LatentAmalgamation.diagonal
  -- `Comparison.lean`: the set identity (4.62) that Theorem 4.15's missing induction runs
  -- on.  The paper writes `F_i` for `contribIdx i` and never defines it (errata entry 5).
  Condensation.iInter_contribIdx_eq_above
  -- `Quantitative.lean`: the conditional interaction-information symmetries Lemma 5.4 is
  -- proved through, the polar's lattice facts, and the `ITree`/`LTree` machinery behind
  -- Definition 5.6 and Proposition 5.7.  `kSubsets` is Corollary 5.10's family `F`; the
  -- node is `polar_kSubsets`, inventoried above.
  Condensation.condEntropy_pair_rotate Condensation.condInteractionInfo_comm
  Condensation.condInteractionInfo_swap Condensation.condInteractionInfo_rotate
  Condensation.mem_polar Condensation.mem_polar_iff Condensation.isUpperSet_polar
  Condensation.polar_antitone Condensation.polar_singleton Condensation.polar_eq_iInter
  Condensation.polar_empty
  Condensation.isUpperSet_inf_closed
  Condensation.ITree.leaves Condensation.ITree.subtrees
  Condensation.ITree.label_mem_of_labelsIn Condensation.ITree.label_eq_polar
  Condensation.ITree.decorate
  Condensation.LTree Condensation.LTree.rootLabel Condensation.LTree.erase
  Condensation.LTree.IsIntersectionTree Condensation.LTree.LabelsIn
  Condensation.ITree.labelsIn_decorate Condensation.existsUnique_intersectionTree_ambient
  Condensation.kSubsets
  -- `Examples.lean`, §3.1 witnesses.  `coinCollapse` is a morphism that genuinely changes
  -- the index set; `pairCoinHom₁`/`pairCoinHom₂` are Definition 3.9's remark made concrete
  -- -- a.e.-equal morphisms whose `f` components differ, which is possible because `X` need
  -- not be surjective onto its range type.
  Condensation.coinCollapse Condensation.coinObj Condensation.twoCoinObj
  Condensation.coinCollapseArrow
  Condensation.pairCoinModel Condensation.pairCoinHom₁ Condensation.pairCoinHom₂
  -- M2 close-out (2026-08-18): the generic machinery the four M2 proof shards needed.
  -- Each shard owned a single file, so these landed in "TO BE MOVED" sections of
  -- `Comparison.lean` / `Quantitative.lean` / `Examples.lean` and were relocated to their
  -- proper homes in this pass; they are listed here, not in the inventory above, because
  -- none of them is a numbered node.
  --
  -- `Probability.lean`, beside the rest of the `AEFunctionOf` API and the §2 entropy
  -- substrate.  `congr_left`/`congr_right` transport a dependence across an a.e. equality
  -- of the independent/dependent variable respectively -- `congr_right` is what consumes
  -- `LatentAmalgamation.comm`, reconciling Definition 4.12's `π̃₂` with Theorem 5.8's `π̃₁`.
  -- The three `condEntropy_*_of_aeFunctionOf` lemmas are the conditional analogues of
  -- `entropy_le_of_aeFunctionOf`; the two `_of_subsingleton` lemmas are the companions of
  -- `condEntropy_eq_entropy_of_subsingleton` above, for a *conditioned* variable of
  -- subsingleton range (Example 4.1's guarded-subtype encoding of "let `Y_A` be constant").
  Condensation.AEFunctionOf.congr_left Condensation.AEFunctionOf.congr_right
  Condensation.AEFunctionOf.prodMk_left
  Condensation.condEntropy_congr_of_aeFunctionOf
  Condensation.condEntropy_le_condEntropy_of_aeFunctionOf
  Condensation.condEntropy_le_of_aeFunctionOf
  Condensation.entropy_eq_zero_of_subsingleton Condensation.condEntropy_eq_zero_of_subsingleton
  -- `Model.lean`, beside the Definition 3.4 auxiliaries and the other index-family facts.
  -- `functionOf_jointOn_union` is the union companion of `functionOf_jointOn_mono` above;
  -- `above_mono` is antitonicity of the upward cones; `isUpperSet_iInter_contribIdx` is the
  -- invariant Theorem 4.15's induction carries, so that Proposition 4.10 applies at each
  -- step.
  Condensation.RVModel.functionOf_jointOn_union
  Condensation.above_mono Condensation.isUpperSet_iInter_contribIdx
  -- `ChainRule.lean`: the `famFinset` restatement of `entropy_jointOn_eq_sum_of_iIndepFun`
  -- above, which is the form §4's clients rewrite with.  It replaces three `private`
  -- lemmas that had been re-proved independently in `Examples.lean`.
  Condensation.RVModel.entropy_jointOn_eq_sum_famFinset
  -- `Amalgamation.lean`: `symm` reads an amalgamation of `L₁` with `L₂` backwards, which is
  -- the paper's "using the symmetry of the situation to interchange `Y` and `Z`".  The two
  -- `condScore_lat` lemmas transfer Definition 3.3's `χ` along `ρₖ`; they are what let
  -- Corollary 4.6 and Theorem 4.9 be applied to `L̃ₖ` rather than to `Lₖ`, which is
  -- necessary because R2-F12/F20 deleted the `ρₖ_π` fields and left no relation between
  -- `Lₖ.π ∘ ρₖ` and `π̃ₖ`.  `finiteEntropyOf'` is the same instance as
  -- `RVModel.finiteEntropyOf` with the sample space spelled `Λ₀`; the spelling is
  -- load-bearing, since `lat₁`/`rv₁` are plain `def`s that instance search will not unfold.
  Condensation.LatentAmalgamation.symm
  Condensation.LatentAmalgamation.condScore_lat₁ Condensation.LatentAmalgamation.condScore_lat₂
  Condensation.LatentAmalgamation.finiteEntropyOf'
  -- `Comparison.lean`: the `PerfectlyCondenses` companions of the two `condScore_lat`
  -- lemmas.  They stay here rather than moving to `Amalgamation.lean` with the rest,
  -- because Definition 4.3 lives in `Perfect.lean`, which `Amalgamation.lean` does not
  -- import.
  Condensation.LatentAmalgamation.perfectlyCondenses_lat₁
  Condensation.LatentAmalgamation.perfectlyCondenses_lat₂

-- Factored Space Models: the consumer-surface conveniences advertised in
-- `FactoredSpaces/API.lean` that are not paper endpoints; a subset of them is exercised by
-- `APITests`.  Auto-generated field projections (`Distr.mass`, `.nonneg`, `.sum_eq_one`)
-- are not listed, matching the Finite Factored Sets register above; `Distr` and the two
-- trail structures are, because the boundary advertises the types themselves and their
-- fields are frozen separately by `#assert_fields`.
open FactoredSpaces in
#assert_axioms_clean
  -- §4.1: the ambient factored space and the splice calculus (`dd:pi-space`, `dd:splice`).
  -- `Pt`, `bg`, `DerivedOn` and `derivedOn_iff` are paper nodes and stay in the inventory
  -- above; these are the surrounding vocabulary a client actually writes with.
  PtOn proj projSet proj_eq_restrict splice prodSplit mem_splice_iff splice_eq_cyl_inter
  splice_compl fiber pair indic
  DerivedOn.trans DerivedOn.mono DerivedOn.pair DerivedOn.comp_left
  -- §4.2: the corners and working forms of Definitions 4.5/4.6 and the membership
  -- criteria for `history` that every §5 proof and every client runs on.
  Disintegrates.compl disintegrates_univ disintegrates_empty disintegrates_univ_set
  generates_iff generates_univ generates_iff_history_subset
  history_mono_of_derived history_bg_subset mem_history_bg_of_mem_history
  mem_history_of_sep mem_history_iff_exists_ne exists_ne_of_mem_history
  eventHistory inter_eq_splice
  -- §4.3: the symmetry a client needs before Definition 4.10 is usable.
  StructIndepGiven.symm
  -- Probability substrate (`dd:dist`).  `Distr` itself, its `@[ext]` lemma, the whole
  -- `prob` calculus, and the constructions (`map`, `delta`, `uniform`, `mix`, `prod`,
  -- `margAt`, `outerCompl`, `condDist`, `cyl`, `sliceAt`) with the transport equivalences
  -- `splitEquiv`/`unionEquiv`/`unionComplEquiv`.  None of these is a paper node; the nodes
  -- they support (Definitions 4.3, 4.4, C.1, C.2) are inventoried above.
  Distr Distr.ext Distr.prob Distr.prob_nonneg Distr.prob_univ Distr.prob_empty
  Distr.prob_mono Distr.prob_le_one Distr.prob_union_of_disjoint Distr.prob_singleton
  Distr.prob_eq_sum_filter Distr.prob_eq_sum_fiber Distr.prob_pos_iff
  Distr.prob_eq_zero_iff Distr.prob_eq_zero_of_subset
  Distr.support Distr.condProb Distr.StrictlyPositive
  Distr.map Distr.map_mass Distr.map_prob Distr.map_map
  Distr.delta Distr.delta_mass Distr.delta_prob Distr.support_delta Distr.delta_eq_prod
  Distr.uniform Distr.uniform_strictlyPositive Distr.mix Distr.euclDist
  Distr.euclDist_self Distr.euclDist_comm Distr.euclDist_nonneg Distr.abs_sub_le_euclDist
  Distr.nonempty_carrier condDist condDist_mass condDist_prob
  Distr.prod Distr.prod_mass Distr.prod_mass_pos_iff Distr.prob_prod_agree_on
  Distr.prob_prod_inter_bg Distr.margAt Distr.margAt_prod
  factorizing factorizingPos factorizes_iff_exists_prod factorizes_prod
  Factorizes.eq_prod_margAt factorizes_delta
  Distr.outerCompl Distr.outerCompl_mass Factorizes.eq_outerCompl Factorizes.marg_mass
  outerCompl_delta_eq_prod cyl sliceAt splitEquiv unionEquiv unionComplEquiv
  -- §6.1 and Appendix C: the mixed conditional-independence forms, the two directions of
  -- Theorem 6.2 isolated from the iff (which is how a client consumes it), the
  -- interpolation, and the general form of Lemma C.17.
  CondIndepEventVar CondIndepVarEvent CondIndepAll CondIndep.symm CondIndep.of_prob_eq_zero
  fiber_pair condIndepVar_of_structIndepGiven structIndepGiven_of_forall_condIndepVar
  condIndepVarEvent_proj_of_disintegrates
  interp interp_zero interp_one factorizes_interp pairsDifferingAt mem_cohistory_iff
  -- §5.1: the carrier of Definition 5.1's axioms and the two relations Proposition 5.2
  -- and Theorem 6.2 instantiate it at.
  IndepRel structIndepRel condIndepRel
  -- §5.2, graph side (root `Digraph` namespace): acyclicity and its one-line consequences,
  -- ancestry, parents, and the depth/ancestral-closure order the chain rule of
  -- `factorizesOverDAG_of_isIMapDAG` runs on.
  Digraph.IsAcyclic Digraph.IsAcyclic.wf Digraph.IsAcyclic.ne_of_adj
  Digraph.IsAcyclic.not_adj_symm Digraph.IsAcyclic.not_ancestor_of_adj
  Digraph.IsAncestor Digraph.parents Digraph.mem_parents Digraph.notMem_parents_self
  Digraph.depth Digraph.depth_lt Digraph.depth_lt_of_isAncestor Digraph.AncClosed
  -- §5.2, construction side: `Ω^G` and the node variables, with the reading-off API, plus
  -- the CPD vocabulary and the components of `τ`.  The Lemma 5.3 / Propositions 5.4, 5.6
  -- statements themselves are inventoried above.  `mem_history_nodeVar_iff` is the closed
  -- form of `H(X_v)` that Proposition 5.6 is read off from (`FactoredSpaces/Separation.lean`).
  ParentVals parentConfig bnIndex bnFactor nodeVar nodeVar_apply nodeVar_eq_of_diag
  jointVar_eq_iff constTable jointVar_constTable jointVar nodesVar famVar famJoint
  CPD FactorizesOverDAG dagFactorizing condCPD tau tauInv tauPos mem_history_nodeVar_iff
  -- d-separation (`dd:dsep`): the definition itself is not a paper node (the paper does not
  -- define it, errata E8), so all of it lives here — trails, collider status, activity, the
  -- `Z`-closure criterion, and the local Markov property.
  Digraph.Trail Digraph.Walk Digraph.Walk.IsColliderAt Digraph.Walk.Active
  Digraph.Trail.Active Digraph.ColliderOK Digraph.DSeparated Digraph.Trail.nil
  Digraph.Trail.nil_active_iff Digraph.not_dSeparated_self
  Digraph.dSeparated_iff_forall_singleton Digraph.dSeparated_singleton_parents
  Digraph.dSeparated_iff_disjoint_zClosureSet
  -- §5.2.3: the I-map weakening of Definition 5.7(1) and the theorem the paper's proof of
  -- Proposition 5.8(1) omits (errata E7).
  IsIMapDAG factorizesOverDAG_of_isIMapDAG
  -- The witness objects of `FactoredSpaces/Examples.lean` the API advertises by name; the
  -- facts proved about them are inventoried above.
  Examples.Coins Examples.diag Examples.G₁ Examples.Q
  Examples.Pdiag Examples.G₀
  -- The `Z`-closure vocabulary of `ConditionalHistory.lean` (root `Digraph` namespace).
  -- `dSeparated_iff_disjoint_zClosureSet` above is *stated* in it, so a client cannot use
  -- that criterion without these names; `Skel` and `Trail.toWalk` are what writing a
  -- concrete trail down and reading its collider status take; and
  -- `exists_active_trail_of_active_walk` is the walk-to-trail bridge the `dd:owalk`
  -- glossary cites, which lets a client define d-separation through walks instead.
  Digraph.unblockedAnc
  Digraph.IsZClosed
  Digraph.zClosure
  Digraph.zClosureSet
  Digraph.zClosure_subset
  Digraph.mem_zClosureSet_self
  Digraph.mem_zClosureSet_of_mem_unblockedAnc
  Digraph.exists_of_mem_zClosureSet
  Digraph.Skel
  Digraph.Trail.toWalk
  Digraph.exists_active_trail_of_active_walk
  -- Small tools `APITests` uses that the bullets above did not name: the `Ω^G` index at a
  -- joint value and the transport that keeps its dependent argument out of a rewrite, the
  -- mass of the Lemma 5.3 pushforward, and the support-membership criterion.
  idxAt
  table_congr
  tau_mass
  Distr.mem_support_iff
  -- The two general d-separation discharge routes and the one-edge trail they are checked
  -- against (`FactoredSpaces/DSeparation.lean`), plus the §6.1 conditional-independence
  -- tools a client needs to verify Definition 5.7 by hand over arbitrary, possibly
  -- overlapping triples, and the transport of a conditional independence along a
  -- pushforward (`FactoredSpaces/Probability.lean`).
  Digraph.dSeparated_of_subset_left
  Digraph.dSeparated_of_subset_right
  Digraph.Trail.pair
  Digraph.Trail.pair_active
  Digraph.not_dSeparated_of_skel
  CondIndep.of_subset_left
  CondIndep.of_disjoint_left
  CondIndepVar.symm
  fiber_proj_subset_or_disjoint
  condIndepVar_proj_of_subset_left
  condIndepVar_proj_of_subset_right
  CondIndepVar.of_proj_subset
  not_condIndepVar_proj_self
  condIndepVar_map
  -- The new witness objects `FactoredSpaces/API.lean` advertises by name.
  Examples.G₂
  Examples.Pedge