FilesExpand file tree

main

/

Reflections

/

Copy path

Directory actions

More options

More options

Directory actions

More options

More options

Latest commit

 

History

History

History

main

/

Reflections

/

Copy path

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
AbsorbedBinderSplitDepth.lean		AbsorbedBinderSplitDepth.lean
AdditiveFieldCostByKeying.lean		AdditiveFieldCostByKeying.lean
AdditiveFieldForcesProducerMutualRecursion.lean		AdditiveFieldForcesProducerMutualRecursion.lean
AdditiveParallelGuard.lean		AdditiveParallelGuard.lean
AdditiveParallelType.lean		AdditiveParallelType.lean
AdjacencyMirrorCornerIsLayerScoped.lean		AdjacencyMirrorCornerIsLayerScoped.lean
AdjacentOriginReconstructs.lean		AdjacentOriginReconstructs.lean
AdvanceArmBalanceFree.lean		AdvanceArmBalanceFree.lean
AggregateCollapsesStructuredSeparates.lean		AggregateCollapsesStructuredSeparates.lean
AllDepthOverreachSourceGlobally.lean		AllDepthOverreachSourceGlobally.lean
AxisDualFromTypeAgnosticCore.lean		AxisDualFromTypeAgnosticCore.lean
BackwardLocatorMirrorsForward.lean		BackwardLocatorMirrorsForward.lean
BalanceInvisibleSplitGrammarLocated.lean		BalanceInvisibleSplitGrammarLocated.lean
BoundaryBoundRecovery.lean		BoundaryBoundRecovery.lean
BoundaryDischargeGateTriggerTyped.lean		BoundaryDischargeGateTriggerTyped.lean
BoundaryInclusiveNeedsSiblingNotCoercion.lean		BoundaryInclusiveNeedsSiblingNotCoercion.lean
BoundaryInclusiveSiblingCascade.lean		BoundaryInclusiveSiblingCascade.lean
BoundaryResidualEndDual.lean		BoundaryResidualEndDual.lean
BoundaryRobustVsFragileFact.lean		BoundaryRobustVsFragileFact.lean
BracketGuardsAdmitCrossMatched.lean		BracketGuardsAdmitCrossMatched.lean
BridgeDerivableFromInvariant.lean		BridgeDerivableFromInvariant.lean
BundleFreeProjectionIntoProducer.lean		BundleFreeProjectionIntoProducer.lean
CarriedInvariantAdvanceEdge.lean		CarriedInvariantAdvanceEdge.lean
CarrierDomainWiderThanNavigatorReach.lean		CarrierDomainWiderThanNavigatorReach.lean
CarrierProvenanceNotType.lean		CarrierProvenanceNotType.lean
CarryUpSplitsAtImportEdge.lean		CarryUpSplitsAtImportEdge.lean
CarveLeavesToEliminatorOutput.lean		CarveLeavesToEliminatorOutput.lean
CharListSegmentPeel.lean		CharListSegmentPeel.lean
ClimbingPremiseTerminatesAtCaseSplit.lean		ClimbingPremiseTerminatesAtCaseSplit.lean
CoconstructionHalfFoldsToSiblingInput.lean		CoconstructionHalfFoldsToSiblingInput.lean
CoerceToWeakerReuseWrapper.lean		CoerceToWeakerReuseWrapper.lean
CoercionDissolvesForcedProjection.lean		CoercionDissolvesForcedProjection.lean
ComplementGuardNotSufficient.lean		ComplementGuardNotSufficient.lean
ComposeArmSeamBeforeSkeleton.lean		ComposeArmSeamBeforeSkeleton.lean
ComposeMapPairsPointwise.lean		ComposeMapPairsPointwise.lean
ComposeSeqItemsPointwise.lean		ComposeSeqItemsPointwise.lean
ConjunctionMergeCostIsCitationEdges.lean		ConjunctionMergeCostIsCitationEdges.lean
ConjunctionMotiveBreaksProducerCycle.lean		ConjunctionMotiveBreaksProducerCycle.lean
ConjunctiveConsumerGatesOnOrthogonalAxis.lean		ConjunctiveConsumerGatesOnOrthogonalAxis.lean
ConstructorFieldForcesMutualGroupMerge.lean		ConstructorFieldForcesMutualGroupMerge.lean
ConsumerJointBeforeProducer.lean		ConsumerJointBeforeProducer.lean
ContainedFrameIHFromOuterIH.lean		ContainedFrameIHFromOuterIH.lean
ContainmentFromFloorConflict.lean		ContainmentFromFloorConflict.lean
ContentListStepAlgebra.lean		ContentListStepAlgebra.lean
ContentSurfacingLocatorTwin.lean		ContentSurfacingLocatorTwin.lean
ContextFreeAdapterKnot.lean		ContextFreeAdapterKnot.lean
ContradictionBranchSuppliesBoundary.lean		ContradictionBranchSuppliesBoundary.lean
ContravariantGuardStrengthening.lean		ContravariantGuardStrengthening.lean
ConvergentReduction.lean		ConvergentReduction.lean
ConverseForwardAsymmetry.lean		ConverseForwardAsymmetry.lean
CrossFrameStructuralDescent.lean		CrossFrameStructuralDescent.lean
CycleBreaksAtBase.lean		CycleBreaksAtBase.lean
DeepConjunctRootSeedOnly.lean		DeepConjunctRootSeedOnly.lean
DeepFamilyMirrorsFullMutualGroup.lean		DeepFamilyMirrorsFullMutualGroup.lean
DeepNavigatorFires.lean		DeepNavigatorFires.lean
DeferredStructuralAlreadyProvenBySibling.lean		DeferredStructuralAlreadyProvenBySibling.lean
DeferredTypedFactInGuard.lean		DeferredTypedFactInGuard.lean
DelegatedNestingShedsGuardFields.lean		DelegatedNestingShedsGuardFields.lean
DelegationTreeCollapsesFieldRipple.lean		DelegationTreeCollapsesFieldRipple.lean
DeliverableContractBeforeProducerBody.lean		DeliverableContractBeforeProducerBody.lean
DeltaGenericBoundaryFamily.lean		DeltaGenericBoundaryFamily.lean
DemotedDispatchMetricFromStructure.lean		DemotedDispatchMetricFromStructure.lean
DepthGateRestrictionDiagnostic.lean		DepthGateRestrictionDiagnostic.lean
DepthGeneralMatchingClose.lean		DepthGeneralMatchingClose.lean
DepthHypCostIsItsEqualityReads.lean		DepthHypCostIsItsEqualityReads.lean
DeriskedMigrationOneClonePerConsumer.lean		DeriskedMigrationOneClonePerConsumer.lean
DescendStepConsumerJoint.lean		DescendStepConsumerJoint.lean
DescendStrengthInvariant.lean		DescendStrengthInvariant.lean
DescendTailDualUseSeparatorSuccessor.lean		DescendTailDualUseSeparatorSuccessor.lean
DescopeIsRouteRelative.lean		DescopeIsRouteRelative.lean
DispatchFirstEntryToWholeWindow.lean		DispatchFirstEntryToWholeWindow.lean
DispatchPinsLocatedDepth.lean		DispatchPinsLocatedDepth.lean
DispatchRoleFactorsTypeMetric.lean		DispatchRoleFactorsTypeMetric.lean
DockImportsConclusionProbesThreadedHyps.lean		DockImportsConclusionProbesThreadedHyps.lean
DomainRestrictionPreservationNegation.lean		DomainRestrictionPreservationNegation.lean
DownstreamDeriskRestoresUpstream.lean		DownstreamDeriskRestoresUpstream.lean
DownstreamProjectionRebuildFromConstituents.lean		DownstreamProjectionRebuildFromConstituents.lean
DroppedBranchGuardMisMeasuresRecursion.lean		DroppedBranchGuardMisMeasuresRecursion.lean
EdgeAdjacentReadFromGlobal.lean		EdgeAdjacentReadFromGlobal.lean
EdgesUnifyAsDeliverableProjection.lean		EdgesUnifyAsDeliverableProjection.lean
EmissionIntercalate.lean		EmissionIntercalate.lean
EmitProducerStrengthening.lean		EmitProducerStrengthening.lean
EmitterTagPercentDecode.lean		EmitterTagPercentDecode.lean
EmptyNodePropsSeqEntry.lean		EmptyNodePropsSeqEntry.lean
EnclosingFrameRekeysWidthRecursion.lean		EnclosingFrameRekeysWidthRecursion.lean
EndFreeGateUnderdeterminesClose.lean		EndFreeGateUnderdeterminesClose.lean
EntryBoundaryLocator.lean		EntryBoundaryLocator.lean
EscapedTrailingTab.lean		EscapedTrailingTab.lean
FieldAuditLocalizesKnot.lean		FieldAuditLocalizesKnot.lean
FieldOnMultiproducerPredicate.lean		FieldOnMultiproducerPredicate.lean
FloorBlindGateAdmitsCrossSibling.lean		FloorBlindGateAdmitsCrossSibling.lean
FloorEncodesNonemptiness.lean		FloorEncodesNonemptiness.lean
FlowMapLoopPairAt.lean		FlowMapLoopPairAt.lean
FlowMapLoopWitness.lean		FlowMapLoopWitness.lean
FlowSeqLoopValueAt.lean		FlowSeqLoopValueAt.lean
FlowSeqLoopWitness.lean		FlowSeqLoopWitness.lean
FoldConsumerChain.lean		FoldConsumerChain.lean
FreeProjectionInvariant.lean		FreeProjectionInvariant.lean
FromLocatedAssemblerDirection.lean		FromLocatedAssemblerDirection.lean
GateTokenIsSiblingHead.lean		GateTokenIsSiblingHead.lean
View all files