Chapter 17 Companion Checks
Back to Content
The monoidal repair for Chapter 17 has two companion checks.
Lean
These commands rebuild the local Mathlib workspace and re-run the mechanized laws named in the manuscript:
cd open-source/gnosis
lake build GnosisProofs
lake env lean GnosisProofs.leanThe relevant theorems live in GnosisProofs.lean:
tensor_interchangerace_tree_coherencefold_tree_coherencec3_deterministic_foldspectrallyStable_of_nilpotentspectrallyStable_of_rowMasssupportPath_reachesSmallSet_of_distanceWitnessfiniteSmallSetRecurrent_of_distanceWitnesscountableSupportPath_reachesSmallSet_of_driftWitnesscountableSmallSetRecurrent_of_driftWitnesscountableAtomicSmallSetMinorized_one_of_collapsecountableAtomAccessibleAt_of_smallSetRecurrence_and_atomicMinorizationcountablePsiIrreducibleAt_of_atomAccessiblecountableHarrisPreludeAt_of_componentscountableHarrisRecurrentClassAt_of_recurrence_and_preludecountableGeometricEnvelopeAt_of_harrisPrelude_and_boundcountableAtomAccessible_of_smallSetRecurrence_and_atomicMinorizationcountablePsiIrreducibleAtAtom_of_atomAccessiblecountableHarrisPreludeAtAtom_of_componentscountableHarrisRecurrentClassAtAtom_of_recurrence_and_preludecountableAtomHittingBoundAtAtom_of_minorizationcountableGeometricEnvelopeAtAtom_of_harrisPrelude_and_boundcountableAtomGeometricHitLowerBoundAtAtom_of_minorizationcountableQuantitativeGeometricEnvelopeAtAtom_of_componentscountableLaminarGeometricStabilityAtAtom_of_componentsmeasurableHarrisPrelude_of_componentsmeasurableHarrisPrelude_of_reversiblemeasurableHarrisPrelude_of_le_referenceMeasuremeasurableSmallSetAccessible_of_irreduciblemeasurableReferencePositiveAccessible_of_irreduciblemeasurableHarrisCertified_of_preludemeasurableIrreducible_dirac_of_atomAccessiblemeasurableHarrisCertified_of_atomAccessiblemeasurableSmallSetAccessible_of_atomAccessiblemeasurableContainingAtomAccessible_of_atomAccessiblemeasurableLaminarCertifiedAtAtom_of_atomAccessiblemeasurableSmallSetAccessible_of_laminarCertifiedAtAtommeasurableContainingAtomAccessible_of_laminarCertifiedAtAtomdeterministic_pow_eq_deterministic_iteratemeasurableAtomAccessible_of_deterministic_hitnat_iterate_queueStep_hits_atomnatMeasurableAtomAccessible_of_queueStepnatQueueSupportInvariantAtAtomnatQueueSupportSmallSetMinorizednatMeasurableHarrisCertified_of_queueStepnatMeasurableLaminarCertified_of_queueStepnatMeasurableAtomHittingBound_of_queueStepnatMeasurableQuantitativeLaminarCertified_of_queueStepnatMeasurableQuantitativeHarrisCertified_of_queueStepnatMeasurableEventuallyConvergesToAtom_of_queueStepnatMeasurableFiniteTimeHarrisRecurrent_of_queueStepnatQueueWitnessKernelnatMeasurableAtomAccessible_of_queueWitnessKernelnatMeasurableAtomHittingBound_of_queueWitnessKernelnatMeasurableHarrisCertified_of_queueWitnessKernelnatMeasurableLaminarCertified_of_queueWitnessKernelnatMeasurableQuantitativeLaminarCertified_of_queueWitnessKernelnatMeasurableQuantitativeHarrisCertified_of_queueWitnessKernelmeasurableContainingAtomHittingBound_of_quantitativeLaminarCertifiedAtAtommeasurableSmallSetHittingBound_of_quantitativeLaminarCertifiedAtAtommeasurableReferencePositiveHittingBound_of_quantitativeLaminarCertifiedAtAtommeasurableQuantitativeHarrisCertified_of_quantitativeLaminarCertifiedAtAtommeasurableReferencePositiveRecurrent_of_harrisCertifiedmeasurableHarrisRecurrent_of_harrisCertifiedmeasurableQuantitativeReferencePositiveRecurrent_of_quantitativeHarrisCertifiedmeasurableReferencePositivePersistent_of_eventualConvergencemeasurableReferencePositivePersistent_of_finiteTimeHarrisRecurrentmeasurableFiniteTimeGeometricStability_of_finiteTimeHarrisRecurrentmeasurableFiniteTimeGeometricEnvelope_of_finiteTimeHarrisRecurrentmeasurableHarrisRecurrent_of_finiteTimeHarrisRecurrentmeasurableFiniteTimeGeometricErgodic_of_finiteTimeHarrisRecurrentmeasurableLevyProkhorovEventuallyZero_of_eventualConvergencemeasurableLevyProkhorovEventuallyZero_of_finiteTimeHarrisRecurrentmeasurableFiniteTimeLevyProkhorovGeometricErgodic_of_finiteTimeHarrisRecurrentmeasurableLevyProkhorovGeometricDecayAfterBurnIn_of_eventualConvergencemeasurableLevyProkhorovGeometricDecayAfterBurnIn_of_finiteTimeHarrisRecurrentmeasurableLevyProkhorovGeometricErgodic_of_decayAfterBurnInmeasurableLevyProkhorovGeometricErgodic_of_finiteTimeHarrisRecurrentMeasurableContinuousHarrisWitnessnatQueueAffineObservablenatQueueAffineExpectedObservablenatMeasurableLyapunovDriftWitness_of_queueStep_with_gapnatMeasurableContinuousHarrisWitness_of_queueStep_with_gapmeasurableFiniteTimeHarrisRecurrent_of_quantitativeHarris_and_convergencenatSmallSetRecurrent_of_stepDownnatSmallSetRecurrent_of_uniformPredecessorMinorizationnatSmallSetRecurrent_of_margin_stepcertifiedKernel_stablecertifiedKernel_stable_of_drift_certificatedriftAt_coupledArrivalCertificatecoupledArrivalCertificate_negative_driftcoupledCertifiedKernel_stabletetheredCertifiedKernels_stable
Betti
Betti's Lean artifact emission should still pass after the proof workspace changes:
bun test open-source/gnosis/src/betty/lean.test.tsThis confirms that the compiler's generated proof artifact now emits a real CertifiedKernel witness that imports the shared proof workspace instead of relying on a local Unit/axiom scaffold, that the measurable queue artifact reaches the emitted exact-convergence, post-burn-in geometric-decay, and abstract geometric-ergodicity Lévy-Prokhorov endpoints as well as the earlier Harris-style endpoints, that the queue-family bridge now emits bounded affine *_measurable_observable, *_measurable_observable_drift, and *_measurable_continuous_harris_certified theorems over the queue-support kernel, and that the shared proof surface now also carries the bounded coupled-kernel handoff theorem for inter-app arrival pressure.