| Location | Topic | Lean modules |
|---|---|---|
| 1.3 | Limit universal property | ViewSections |
| 1.4 | Functorial transport | ViewSections |
| 1.5 | Terminal evaluation | ViewSections |
| 2.1 | Strict section gluing | SectionGluing |
| 2.2 | Object-only cover failure | ViewBoundaryExamples |
| 2.3 | Correspondence fibers | ViewCorrespondence |
| 2.4 | Nonempty fibers without a section | ViewBoundaryExamples |
| 3.1 | Additive view differential | SectionObstruction |
| 3.2 | Additive extension criterion | SectionObstruction |
| 3.3 | Extension ambiguity torsor | SectionExtensionFibers |
| Source passage | Parity seed example | SectionExtensionExample |
| 3.5 | Exactness at partial sections | SectionExactSequence |
| Source passage | Extension by stages | SectionExtensionStages |
| 4.1 | Protected correction | Correction |
| 4.2 | Obstruction witness | Correction |
| 6.1 | Exact tower maps and realized points | Towers Realization |
| 6.2 | Tower differential composition | Towers TowerCorrection |
| 6.3 | Cofinal point equivalence | Cofinal |
| 8.1 | Geometric operator repair | RepairDynamics RepairProjection |
| 8.2 | Constructed split tower correction | SplitTowerRepair |
| 8.3 | Split semantic and residual coordinates | SplitTowerCoordinates SplitTowerSemantics |
| 8.4 | Growing identity repair | GrowingTower |
| Source passage | A bounded residual without bounded primitive | IdentityTowerObstruction |
| Source passage | Dependence on target splitting | SplittingDependence |
| Source passage | Lossless dyadic residual split | DyadicResidualSplit |
| 10.1 | Cascade telescope and persistent part | CascadeProjections CoarseningCascade |
| 10.2 | Recovery by density | CascadeDensity |
| 10.3 | Dyadic finite-coordinate recovery | DyadicInfiniteReconstruction |
| 10.5 | Shift cascade and c0 | SequenceCascade |
| 11.2 | Gauge groupoid and section transport | GroupViewSystems CocycleGaugeGroupoid |
| 11.3 | Nonabelian extension obstruction | NonabelianExtension |
| 11.4 | Nonabelian extension torsor | NonabelianExtensionFibers |
| 11.5 | S3 loop model | CocycleExamples |
| 12.1 | Effective groupoid descent | DescentEquivalence DescentComparison |
| 13.1 | Composition topology | CompositionSite |
| 13.2 | Standard stackhood | CompositionStack |
| 14.1 | Equivalent view presentations | SectionViewEquivalence RelativeSections RelativeAmbiguity |
| 14.3 | Identified-boundary realization groupoid | MarkedRealization |
| 14.4 | Marked transport across a square | MarkedTransport |
| 17.1 | Transported path telescope | AmplifiedTransport |
| 17.2 | Holonomy classification | AmplifiedHolonomy |
| 18.1 | Orthogonal exact repair | HilbertKernelProjection |
| 18.2 | Closed range equivalence | HilbertKernelProjection |
| 19.1 | Amplified holonomy gain | AmplifiedRepair HilbertHolonomyRepair |
| Source passage | Flat transport amplification | AmplifiedExamples |
| 20.1 | Two-stage joint projection | QuantitativeDescent |
| 20.2 | Joint closed range | DescentClosedRange |
| 21.1 | Two-sided projector motion | MovingKernelBounds |
| 21.2 | Derived perturbed certificate | SplitKernelPerturbation |
| 21.3 | Transport between moving kernels | SplitKernelPerturbation |
| 21.4 | Exact moving-line example | MovingKernelExamples |
| Source passage | Rank loss and radius endpoint | MovingKernelBounds MovingKernelExamples |
| Source passage | Motion of quantitative descent | MovingDescent |
| 35.1 | Finite prefixes without a point | FinitePrefixBoundary |
| 10.4 | Sharper dyadic support criterion | DyadicSupport |
| 18.3 | Nearest protected Hilbert repair | ProtectedHilbertRepair |
| 35.3 | Finite positive and negative certificates | ProtectedLinearCertificates |
| 35.2 | Finite-fiber inverse-limit existence | FiniteRealizationExistence |
| 5.1 | Obstructions under stronger prescription | ObstructionRestriction |
| 5.2 | Prescribed choices and obstructed intermediate steps | ExtensionChoiceExample |
| 7.1 | Scheduled transports and eventual equality | ReindexedTransports EventualCategory |
| 7.2 | Faithfulness from observable finite stages | RealizationFaithfulness |
| 7.3 | Finite observation characterizes realized transport | FiniteObservation |
| 7.4 | Cofinal transport equivalence | CofinalTransports |
| 9.1 | Split repair coordinates and choice dependence | SplitDefectCharts |
| 9.2 | Triangular representation change and repair mismatch | ResidualNaturality |
| 9.3 | Residual sampling and repair across scales | ResidualSampling SamplingRepair |
| 15.1 | Why literal full framing is presentation dependent | FramingBoundaryExamples |
| 22.1 | Measured and uncertain residual certificates | ResidualPerturbation |
| 22.2 | Stable repair when the old exact space is preserved | ResidualPerturbation |
| 24.1 | Exactification from summable movement | Exactification |
| 24.2 | Variable-rate exactification and posterior bounds | Exactification |
| 24.3 | Controlled approximation annihilates protected obstruction | LinearExactification |
| 24.4 | Path comparison and nonunique protected answers | Exactification RepairExamples |
| 24.5 | What cofinal residual-profile sampling preserves | Profiles |
| 25.1 | Obstruction floors detect closure, not exact membership | ObstructionFloor |
| 25.2 | Persistent floors exclude all admissible repair sequences | ObstructionFloor |
| 23.1 | Independent transport costs and directed geometry | WeightedGeometry |
| 23.2 | Zero arrows can collapse object distance | WeightedGeometry |
| 16.1 | An associative phase with no scalar flattening | ProjectiveExample |
Komorebi SpaceReading edition
Claim correspondence
Reading tools
Reading libraryFind statementsInspect Lean
Text settings
Saved in this browser for reading chapters. Browser zoom also works.
Source and conversion record
Source SHA-256: a1028b1ccd6062d0fbff35bc4cfe52c6694f0d3e70aaac3a1af78e0cc0cb02ad
Unsupported prose commands stop the build. The mathematical expression sequence is checked against the source, with manuscript macros expanded for display.