HeytingLean Blueprint
0.1 Overview
This is the initial blueprint for the HeytingLean library. Click “Dependency graph” in the left sidebar, or open the dependency graph page.
For the full module import structure extracted from the Lean sources, open the system import graph.
0.2 Demo: Labeled Results and Uses
We add a few labeled items and declare their dependencies with \uses{...}.
Basic axiom used throughout the section.
0.3 Auto-generated Module Dependencies
0.3.1 Automation
Module HeytingLean.Automation.
Module HeytingLean.Automation.QwenGenerated.
0.3.2 Basic
Module HeytingLean.Basic.
0.3.3 Blockchain
Module HeytingLean.Blockchain.Contracts.CLI.PEGDemo.
Module HeytingLean.Blockchain.Contracts.PEGv0.
Module HeytingLean.Blockchain.Rollup.CLI.Demo.
Module HeytingLean.Blockchain.Rollup.MultiLens.
Module HeytingLean.Blockchain.Rollup.StateTransition.
0.3.4 Bridges
Module HeytingLean.Bridges.Clifford.
Module HeytingLean.Bridges.Clifford.Commutant.
Module HeytingLean.Bridges.Clifford.Projector.
Module HeytingLean.Bridges.Geo.
Module HeytingLean.Bridges.Geo.Examples.
Module HeytingLean.Bridges.Graph.
Module HeytingLean.Bridges.Graph.Alexandroff.
Module HeytingLean.Bridges.RoundTrip.
Module HeytingLean.Bridges.Tensor.
Module HeytingLean.Bridges.Tensor.Intensity.
0.3.5 CCI
Module HeytingLean.CCI.Cert.
Module HeytingLean.CCI.Check.
Module HeytingLean.CCI.Core.
Module HeytingLean.CCI.Json.
Module HeytingLean.CCI.RewriteTable.
Module HeytingLean.CCI.Version.
0.3.6 CLI
Module HeytingLean.CLI.CCICheck.
Module HeytingLean.CLI.EmitPublic.
Module HeytingLean.CLI.ExportCCI.
Module HeytingLean.CLI.FormEncExport.
Module HeytingLean.CLI.FormEncExportBin.
Module HeytingLean.CLI.GeoBoolDemo.
Module HeytingLean.CLI.LensDump.
Module HeytingLean.CLI.LoFCanonExample.
Module HeytingLean.CLI.SurrealPGNorm.
Module HeytingLean.CLI.TraceDigest.
Module HeytingLean.CLI.ZKRunner.
Module HeytingLean.CLI.ZKStubDemo.
0.3.7 Computation
Module HeytingLean.Computation.FixedPoint.
0.3.8 Computing
Module HeytingLean.Computing.CircuitClassic.
0.3.9 Contracts
Module HeytingLean.Contracts.Examples.
Module HeytingLean.Contracts.RoundTrip.
Module HeytingLean.Contracts.RoundTripInt.
0.3.10 Crypto
Module HeytingLean.Crypto.AlgRegistry.
Module HeytingLean.Crypto.BoolLens.
Module HeytingLean.Crypto.Commit.
Module HeytingLean.Crypto.Commit.NucleusCommit.
Module HeytingLean.Crypto.Compile.
Module HeytingLean.Crypto.CoreSemantics.
Module HeytingLean.Crypto.CoreTypes.
Module HeytingLean.Crypto.Correctness.
Module HeytingLean.Crypto.Form.
Module HeytingLean.Crypto.FormEncBin.
Module HeytingLean.Crypto.FormJson.
Module HeytingLean.Crypto.Hash.Poseidon.
Module HeytingLean.Crypto.Lattice.Stages.
Module HeytingLean.Crypto.Lens.Class.
Module HeytingLean.Crypto.Lens.Semantics.
Module HeytingLean.Crypto.Lens.Transport.
Module HeytingLean.Crypto.PCT.
Module HeytingLean.Crypto.Prog.
Module HeytingLean.Crypto.ProofSystem.NucleusZK.
Module HeytingLean.Crypto.PublicJson.
Module HeytingLean.Crypto.Trace.
Module HeytingLean.Crypto.VM.
Module HeytingLean.Crypto.Witness.
Module HeytingLean.Crypto.WitnessJson.
Module HeytingLean.Crypto.ZK.AirIR.
Module HeytingLean.Crypto.ZK.Backends.Air.
Module HeytingLean.Crypto.ZK.Backends.Bullet.
Module HeytingLean.Crypto.ZK.Backends.Plonk.
Module HeytingLean.Crypto.ZK.BoolArith.
Module HeytingLean.Crypto.ZK.BulletIR.
Module HeytingLean.Crypto.ZK.CLI.PCTCheck.
Module HeytingLean.Crypto.ZK.CLI.PCTExport.
Module HeytingLean.Crypto.ZK.CLI.PCTMutate.
Module HeytingLean.Crypto.ZK.CLI.PCTProve.
Module HeytingLean.Crypto.ZK.CLI.PCTR1CS.
Module HeytingLean.Crypto.ZK.CLI.PCTR1CSMain.
Module HeytingLean.Crypto.ZK.CLI.PCTReverseR1CS.
Module HeytingLean.Crypto.ZK.CLI.PCTSmoke.
Module HeytingLean.Crypto.ZK.CLI.PCTVerify.
Module HeytingLean.Crypto.ZK.CLI.ProveFromCert.
Module HeytingLean.Crypto.ZK.Export.
Module HeytingLean.Crypto.ZK.Groth16.
Module HeytingLean.Crypto.ZK.IR.
Module HeytingLean.Crypto.ZK.LensProofs.
Module HeytingLean.Crypto.ZK.PlonkIR.
Module HeytingLean.Crypto.ZK.R1CS.
Module HeytingLean.Crypto.ZK.R1CSBool.
Module HeytingLean.Crypto.ZK.R1CSSoundness.
Module HeytingLean.Crypto.ZK.Rename.
Module HeytingLean.Crypto.ZK.Support.
0.3.11 Epistemic
Module HeytingLean.Epistemic.Occam.
0.3.12 Generative
Module HeytingLean.Generative.IntNucleusKit.
Module HeytingLean.Generative.NucleusKit.
Module HeytingLean.Generative.SurrealNucleusKit.
0.3.13 LoF
Module HeytingLean.LoF.ClosureCore.
Module HeytingLean.LoF.ComparisonNucleus.
Module HeytingLean.LoF.ComparisonNucleus.RTTRI.
Module HeytingLean.LoF.ComparisonNucleus.Soundness.
Module HeytingLean.LoF.ComparisonNucleus.Spec.
Module HeytingLean.LoF.Core.
Module HeytingLean.LoF.HeytingCore.
Module HeytingLean.LoF.Instances.
Module HeytingLean.LoF.IntReentry.
Module HeytingLean.LoF.Lens.Clifford.
Module HeytingLean.LoF.Lens.Graph.
Module HeytingLean.LoF.Lens.RoundTrip.
Module HeytingLean.LoF.Lens.Tensor.
Module HeytingLean.LoF.Nucleus.
Module HeytingLean.LoF.NucleusLemmas.
Module HeytingLean.LoF.PrimaryAlgebra.
Module HeytingLean.LoF.RightLeg.
Module HeytingLean.LoF.RightLeg.Instances.
Module HeytingLean.LoF.RightLeg.Selector.
0.3.14 Logic
Module HeytingLean.Logic.Dialectic.
Module HeytingLean.Logic.ModalDial.
Module HeytingLean.Logic.PSR.
Module HeytingLean.Logic.ResiduatedLadder.
Module HeytingLean.Logic.StageSemantics.
Module HeytingLean.Logic.Trace.
Module HeytingLean.Logic.Triad.
0.3.15 Noneism
Module HeytingLean.Noneism.Bridges.HeytingBridge.
Module HeytingLean.Noneism.Examples.RoundSquare.
Module HeytingLean.Noneism.Semantics.Jacquette.
Module HeytingLean.Noneism.Semantics.LP.
Module HeytingLean.Noneism.Semantics.ModalPriest.
Module HeytingLean.Noneism.Semantics.RoutleyMeyer.
Module HeytingLean.Noneism.Semantics.Sylvan.
Module HeytingLean.Noneism.Syntax.
Module HeytingLean.Noneism.Tests.Jacquette.
Module HeytingLean.Noneism.Tests.LP.
Module HeytingLean.Noneism.Tests.ModalPriest.
Module HeytingLean.Noneism.Tests.Paraconsistent.
Module HeytingLean.Noneism.Tests.Sylvan.
0.3.16 Numbers
Module HeytingLean.Numbers.Ordinal.Nucleus.
Module HeytingLean.Numbers.OrdinalVN.
Module HeytingLean.Numbers.Surreal.ClosureReentry.
Module HeytingLean.Numbers.Surreal.ComparisonCore.
Module HeytingLean.Numbers.Surreal.ComparisonDefault.
Module HeytingLean.Numbers.Surreal.ComparisonLoF.
Module HeytingLean.Numbers.Surreal.Embeddings.
Module HeytingLean.Numbers.Surreal.Equiv.
Module HeytingLean.Numbers.Surreal.GameN.
Module HeytingLean.Numbers.Surreal.Instances.
Module HeytingLean.Numbers.Surreal.JClosure.
Module HeytingLean.Numbers.Surreal.Normalized.
Module HeytingLean.Numbers.Surreal.NormalizedPG.
Module HeytingLean.Numbers.Surreal.Nucleus.
Module HeytingLean.Numbers.Surreal.NucleusCore.
Module HeytingLean.Numbers.Surreal.Operations.
Module HeytingLean.Numbers.Surreal.Order.
Module HeytingLean.Numbers.Surreal.OrderNormalized.
Module HeytingLean.Numbers.Surreal.QuotOps.
Module HeytingLean.Numbers.Surreal.ReentryAdapter.
Module HeytingLean.Numbers.SurrealCore.
0.3.17 Ontology
Module HeytingLean.Ontology.Primordial.
0.3.18 Payments
Module HeytingLean.Payments.CLI.PMProve.
Module HeytingLean.Payments.CLI.PMSnarkProve.
Module HeytingLean.Payments.CLI.PMSnarkSetup.
Module HeytingLean.Payments.CLI.PMSnarkVerify.
Module HeytingLean.Payments.CLI.PMTests.
Module HeytingLean.Payments.CLI.PMVerify.
Module HeytingLean.Payments.Commit.
Module HeytingLean.Payments.ContractModel.
Module HeytingLean.Payments.Merkle.
Module HeytingLean.Payments.Rules.
Module HeytingLean.Payments.Types.
0.3.19 ProofWidgets
Module HeytingLean.ProofWidgets.LoFViz.
Module HeytingLean.ProofWidgets.LoFViz.Kernel.
Module HeytingLean.ProofWidgets.LoFViz.Proof.Core.
Module HeytingLean.ProofWidgets.LoFViz.Proof.Graph.
Module HeytingLean.ProofWidgets.LoFViz.Render.Boundary.
Module HeytingLean.ProofWidgets.LoFViz.Render.Fiber.
Module HeytingLean.ProofWidgets.LoFViz.Render.Hypergraph.
Module HeytingLean.ProofWidgets.LoFViz.Render.Models.
Module HeytingLean.ProofWidgets.LoFViz.Render.Router.
Module HeytingLean.ProofWidgets.LoFViz.Render.String.
Module HeytingLean.ProofWidgets.LoFViz.Render.Types.
Module HeytingLean.ProofWidgets.LoFViz.Rpc.
Module HeytingLean.ProofWidgets.LoFViz.State.
Module HeytingLean.ProofWidgets.LoFViz.Tests.
Module HeytingLean.ProofWidgets.LoFViz.Widget.
0.3.20 Runtime
Module HeytingLean.Runtime.BridgeSuite.
0.3.21 Tests
Module HeytingLean.Tests.AirBoolOpsTransition.
Module HeytingLean.Tests.AirEqTransition.
Module HeytingLean.Tests.AirMulTransition.
Module HeytingLean.Tests.AirUnionTransition.
Module HeytingLean.Tests.CCI.Check.
Module HeytingLean.Tests.CCI.Json.
Module HeytingLean.Tests.ComparisonNucleus.RTTRI.
Module HeytingLean.Tests.Compliance.
Module HeytingLean.Tests.Crypto.LatticeStages.
Module HeytingLean.Tests.Generative.IntIterateSmoke.
Module HeytingLean.Tests.Generative.IntNucleusKit.
Module HeytingLean.Tests.Generative.NucleusKit.
Module HeytingLean.Tests.Geo.BoolIndiscrete.
Module HeytingLean.Tests.Geo.RealStandard.
Module HeytingLean.Tests.Lenses.Sanity.
Module HeytingLean.Tests.LoF.NucleusLemmas.
Module HeytingLean.Tests.LoF.NucleusSimp.
Module HeytingLean.Tests.Numbers.Stubs.
Module HeytingLean.Tests.Numbers.SurrealClosureReentry.
Module HeytingLean.Tests.Numbers.SurrealComparisonCore.
Module HeytingLean.Tests.Numbers.SurrealComparisonDefault.
Module HeytingLean.Tests.Numbers.SurrealComparisonLoF.
Module HeytingLean.Tests.Numbers.SurrealComparisonLoFReal.
Module HeytingLean.Tests.Numbers.SurrealIntReentry.
Module HeytingLean.Tests.Numbers.SurrealJClosure.
Module HeytingLean.Tests.Numbers.SurrealNucleusKit.
Module HeytingLean.Tests.Numbers.SurrealOps.
Module HeytingLean.Tests.Numbers.SurrealQOps.
Module HeytingLean.Tests.PCT.
Module HeytingLean.Tests.PEGv0.
Module HeytingLean.Tests.PSRIntegration.
Module HeytingLean.Tests.PlonkSigmaCover.
Module HeytingLean.Tests.PlonkSwap.
Module HeytingLean.Tests.PrimordialDialectic.
Module HeytingLean.Tests.Rename.
Module HeytingLean.Tests.Rollup.LensEquiv.
Module HeytingLean.Tests.Topos.CLI.
Module HeytingLean.Tests.Topos.LocalicSmoke.
Module HeytingLean.Tests.Topos.PresheafSmoke.
Module HeytingLean.Tests.Topos.Scaffold.
Module HeytingLean.Tests.Topos.TypesSite.
Module HeytingLean.Tests.ZK.LensProofs.
0.3.22 Topos
Module HeytingLean.Topos.LTfromNucleus.
Module HeytingLean.Topos.LoFCategory.
Module HeytingLean.Topos.LocalOperator.
Module HeytingLean.Topos.Localic.
Module HeytingLean.Topos.SheafBridges.
0.3.23 Util
Module HeytingLean.Util.Base64.
Module HeytingLean.Util.Iterate.
Module HeytingLean.Util.SHA.