Machine-Native Reasoning · Lean source
MachineTheory.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
The accepted project pins Lean 4.34.0-rc2. The browser checker uses Lean 4.33.0 as a separate experiment, with some required imports unavailable. Reproduce the recorded environment with the retained compiler and dependency instructions. Retained runtime and replay instructions.
Local imports (78)
MachineTheory.lean80 lines
Original source path
MachineTheory.lean1 import MachineTheory.Behavior
2 import MachineTheory.Transfer
3 import MachineTheory.Correction
4 import MachineTheory.Instrument
5 import MachineTheory.Feedback
6 import MachineTheory.Examples
7 import MachineTheory.Bayes
8 import MachineTheory.BayesianLumping
9 import MachineTheory.Refinement
10 import MachineTheory.Block02Examples
11 import MachineTheory.Planning
12 import MachineTheory.PlanningTransport
13 import MachineTheory.PlanningSensor
14 import MachineTheory.PlanningControls
15 import MachineTheory.Variation
16 import MachineTheory.ApproximateHistory
17 import MachineTheory.ApproximateDecision
18 import MachineTheory.ApproximationExamples
19 import MachineTheory.ResponseDecision
20 import MachineTheory.DecisionHistory
21 import MachineTheory.ResponseExamples
22 import MachineTheory.Recipient
23 import MachineTheory.RecipientExecution
24 import MachineTheory.RecipientExamples
25 import MachineTheory.HardPareto
26 import MachineTheory.HardInquiry
27 import MachineTheory.HardExecution
28 import MachineTheory.HardSemantics
29 import MachineTheory.HardExamples
30 import MachineTheory.HardControls
31 import MachineTheory.BinaryStructure
32 import MachineTheory.BinaryDiagnosis
33 import MachineTheory.BinaryExecution
34 import MachineTheory.BinaryCertificate
35 import MachineTheory.BinaryExamples
36 import MachineTheory.Synthesis
37 import MachineTheory.SynthesisQuotient
38 import MachineTheory.SynthesisTrace
39 import MachineTheory.SynthesisProtocol
40 import MachineTheory.SynthesisBudget
41 import MachineTheory.SynthesisExamples
42 import MachineTheory.PrefixScan
43 import MachineTheory.OrderedCompiler
44 import MachineTheory.PrefixSemantics
45 import MachineTheory.PrefixAdmission
46 import MachineTheory.PrefixExamples
47 import MachineTheory.DependencyGraph
48 import MachineTheory.Revision
49 import MachineTheory.RevisionReplay
50 import MachineTheory.RevisionAdmission
51 import MachineTheory.RevisionExamples
52 import MachineTheory.RevisionControls
53 import MachineTheory.ResourcePrices
54 import MachineTheory.WorkloadPricing
55 import MachineTheory.PriceExamples
56 import MachineTheory.PriceRevision
57 import MachineTheory.Lineage
58 import MachineTheory.LineageExamples
59 import MachineTheory.JointReconstruction
60 import MachineTheory.JointReconstructionExamples
61 import MachineTheory.LegalQuotient
62 import MachineTheory.LegalTrace
63 import MachineTheory.LegalQuotientExamples
64 import MachineTheory.FiniteFixedPoints
65 import MachineTheory.SafeEnding
66 import MachineTheory.SafeEndingPolicies
67 import MachineTheory.SafeEndingExamples
68 import MachineTheory.CommonQuotient
69 import MachineTheory.CommonQuotientInterface
70 import MachineTheory.DiscrepancyClosure
71 import MachineTheory.CommonQuotientExamples
72
73 import MachineTheory.PositivePackets
74 import MachineTheory.CoordinatePackets
75 import MachineTheory.PacketTransport
76 import MachineTheory.PositivePacketExamples
77
78 import MachineTheory.PartitionOccupancy
79 import MachineTheory.OccupancyBinary
80 import MachineTheory.OccupancyExamples
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 0a1ee0b7cfafef282139a93443e96ba2e1e7d54824493d2ab8d56858c14a146f